[STATEMENT]
lemma stalk_at_prime_is_iso_to_local_ring_at_prime_aux:
  assumes "is_zariski_open V" and "\<pp> \<in> V" and
    \<phi>: "ring_homomorphism \<phi>
      st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
    and all_eq: "\<forall>U\<in>(top.neighborhoods \<pp>). \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = key_map U s"
  shows "ring_isomorphism \<phi>
st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_isomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
proof (intro ring_isomorphism.intro bijective_map.intro bijective.intro)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 2. Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at
 3. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
show "ring_homomorphism \<phi>
st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (2 subgoals):
 1. Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at
 2. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at
 2. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
show "Set_Theory.map \<phi> st.carrier_stalk (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
by (simp add: ring_homomorphism_def)
[PROOF STATE]
proof (state)
this:
Set_Theory.map \<phi> st.carrier_stalk pi.carrier_local_ring_at

goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
show "bij_betw \<phi> st.carrier_stalk (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
have "inj_on \<phi> st.carrier_stalk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on \<phi> st.carrier_stalk
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "s \<in> st.carrier_stalk" "t \<in> st.carrier_stalk" "\<phi> s = \<phi> t"
[PROOF STATE]
proof (state)
this:
s \<in> st.carrier_stalk
t \<in> st.carrier_stalk
\<phi> s = \<phi> t

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
obtain U s' t' a f b g where FU [simp]: "is_zariski_open U" "\<pp> \<in> U" "s' \<in> \<O> U" "t' \<in> \<O> U"
        and s: "s = st.class_of U s'" "t = st.class_of U t'"
        and s': "s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)"
        and t': "t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)"
        and "a \<in> R" "b \<in> R" "f \<in> R" "g \<in> R" "f \<notin> \<pp>" "g \<notin> \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s' t' a f b g. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>U s' t' a f b g. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain V s' t' where HV: "s = st.class_of V s'" "t = st.class_of V t'"
                            "s' \<in> \<O> V" "t' \<in> \<O> V" "is_zariski_open V" "\<pp> \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V s' t'. \<lbrakk>s = st.class_of V s'; t = st.class_of V t'; s' \<in> \<O> V; t' \<in> \<O> V; is_zariski_open V; \<pp> \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using shrinking_from_belong_stalk
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> st.carrier_stalk; ?t \<in> st.carrier_stalk; \<And>U s' t'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; ?s = st.class_of U s'; t' \<in> \<O> U; ?t = st.class_of U t'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>V s' t'. \<lbrakk>s = st.class_of V s'; t = st.class_of V t'; s' \<in> \<O> V; t' \<in> \<O> V; is_zariski_open V; \<pp> \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) \<open>s \<in> st.carrier_stalk\<close> \<open>t \<in> st.carrier_stalk\<close>)
[PROOF STATE]
proof (state)
this:
s = st.class_of V s'
t = st.class_of V t'
s' \<in> \<O> V
t' \<in> \<O> V
is_zariski_open V
\<pp> \<in> V

goal (1 subgoal):
 1. (\<And>U s' t' a f b g. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = st.class_of V s'
t = st.class_of V t'
s' \<in> \<O> V
t' \<in> \<O> V
is_zariski_open V
\<pp> \<in> V
[PROOF STEP]
obtain U a f b g where HU: "is_zariski_open U" "U \<subseteq> V" "\<pp> \<in> U" "a \<in> R" "f \<in> R" "b \<in> R" "g \<in> R"
          "f \<notin> \<pp>" "g \<notin> \<pp>"
          "\<And>\<qq>. \<qq> \<in> U \<Longrightarrow> f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f"
          "\<And>\<qq>. \<qq> \<in> U \<Longrightarrow> g \<notin> \<qq> \<and> t' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g"
[PROOF STATE]
proof (prove)
using this:
s = st.class_of V s'
t = st.class_of V t'
s' \<in> \<O> V
t' \<in> \<O> V
is_zariski_open V
\<pp> \<in> V

goal (1 subgoal):
 1. (\<And>U a f b g. \<lbrakk>is_zariski_open U; U \<subseteq> V; \<pp> \<in> U; a \<in> R; f \<in> R; b \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>; \<And>\<qq>. \<qq> \<in> U \<Longrightarrow> f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f; \<And>\<qq>. \<qq> \<in> U \<Longrightarrow> g \<notin> \<qq> \<and> t' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using shrinking[of V \<pp> s' t']
[PROOF STATE]
proof (prove)
using this:
s = st.class_of V s'
t = st.class_of V t'
s' \<in> \<O> V
t' \<in> \<O> V
is_zariski_open V
\<pp> \<in> V
\<lbrakk>is_zariski_open V; \<pp> \<in> V; s' \<in> \<O> V; t' \<in> \<O> V; \<And>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> V; \<pp> \<in> V; a \<in> R; f \<in> R; b \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>; \<And>\<qq>. \<qq> \<in> V \<Longrightarrow> f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f; \<And>\<qq>. \<qq> \<in> V \<Longrightarrow> g \<notin> \<qq> \<and> t' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>U a f b g. \<lbrakk>is_zariski_open U; U \<subseteq> V; \<pp> \<in> U; a \<in> R; f \<in> R; b \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>; \<And>\<qq>. \<qq> \<in> U \<Longrightarrow> f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f; \<And>\<qq>. \<qq> \<in> U \<Longrightarrow> g \<notin> \<qq> \<and> t' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zariski_open U
U \<subseteq> V
\<pp> \<in> U
a \<in> R
f \<in> R
b \<in> R
g \<in> R
f \<notin> \<pp>
g \<notin> \<pp>
?\<qq>3 \<in> U \<Longrightarrow> f \<notin> ?\<qq>3 \<and> s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> a f
?\<qq>3 \<in> U \<Longrightarrow> g \<notin> ?\<qq>3 \<and> t' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> b g

goal (1 subgoal):
 1. (\<And>U s' t' a f b g. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. is_zariski_open ?U3
 2. \<pp> \<in> ?U3
 3. ?s'3 \<in> \<O> ?U3
 4. ?t'3 \<in> \<O> ?U3
 5. s = st.class_of ?U3 ?s'3
 6. t = st.class_of ?U3 ?t'3
 7. ?s'3 = (\<lambda>\<qq>\<in>?U3. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3)
 8. ?t'3 = (\<lambda>\<qq>\<in>?U3. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 9. ?a3 \<in> R
 10. ?b3 \<in> R
A total of 14 subgoals...
[PROOF STEP]
show "sheaf_spec_morphisms V U s' \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V U s' \<in> \<O> U
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) HU(1,2) HV(3) map.map_closed sheaf_spec_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V U s' \<in> \<O> U

goal (13 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. ?t'3 \<in> \<O> U
 4. s = st.class_of U (sheaf_spec_morphisms V U s')
 5. t = st.class_of U ?t'3
 6. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3)
 7. ?t'3 = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 8. ?a3 \<in> R
 9. ?b3 \<in> R
 10. ?f3 \<in> R
A total of 13 subgoals...
[PROOF STEP]
show "sheaf_spec_morphisms V U t' \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V U t' \<in> \<O> U
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) HU(1,2) HV(4) map.map_closed sheaf_spec_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V U t' \<in> \<O> U

goal (12 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. s = st.class_of U (sheaf_spec_morphisms V U s')
 4. t = st.class_of U (sheaf_spec_morphisms V U t')
 5. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3)
 6. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 7. ?a3 \<in> R
 8. ?b3 \<in> R
 9. ?f3 \<in> R
 10. ?g3 \<in> R
A total of 12 subgoals...
[PROOF STEP]
show "s = st.class_of U (sheaf_spec_morphisms V U s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = st.class_of U (sheaf_spec_morphisms V U s')
[PROOF STEP]
by (simp add: HU(1-3) HV same_class_from_restrict)
[PROOF STATE]
proof (state)
this:
s = st.class_of U (sheaf_spec_morphisms V U s')

goal (11 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. t = st.class_of U (sheaf_spec_morphisms V U t')
 4. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3)
 5. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 6. ?a3 \<in> R
 7. ?b3 \<in> R
 8. ?f3 \<in> R
 9. ?g3 \<in> R
 10. ?f3 \<notin> \<pp>
A total of 11 subgoals...
[PROOF STEP]
show "t = st.class_of U (sheaf_spec_morphisms V U t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = st.class_of U (sheaf_spec_morphisms V U t')
[PROOF STEP]
by (simp add: HU(1-3) HV same_class_from_restrict)
[PROOF STATE]
proof (state)
this:
t = st.class_of U (sheaf_spec_morphisms V U t')

goal (10 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3)
 4. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 5. ?a3 \<in> R
 6. ?b3 \<in> R
 7. ?f3 \<in> R
 8. ?g3 \<in> R
 9. ?f3 \<notin> \<pp>
 10. ?g3 \<notin> \<pp>
[PROOF STEP]
show "sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)
[PROOF STEP]
using HV(3)  sheaf_spec_morphisms_def HU(10)
[PROOF STATE]
proof (prove)
using this:
s' \<in> \<O> V
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V
?\<qq>3 \<in> U \<Longrightarrow> f \<notin> ?\<qq>3 \<and> s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> a f

goal (1 subgoal):
 1. sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V U s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)

goal (9 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3)
 4. a \<in> R
 5. ?b3 \<in> R
 6. f \<in> R
 7. ?g3 \<in> R
 8. f \<notin> \<pp>
 9. ?g3 \<notin> \<pp>
[PROOF STEP]
show "sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
[PROOF STEP]
using HV(4) HU(11) sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
using this:
t' \<in> \<O> V
?\<qq>3 \<in> U \<Longrightarrow> g \<notin> ?\<qq>3 \<and> t' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> b g
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V

goal (1 subgoal):
 1. sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V U t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)

goal (8 subgoals):
 1. is_zariski_open U
 2. \<pp> \<in> U
 3. a \<in> R
 4. b \<in> R
 5. f \<in> R
 6. g \<in> R
 7. f \<notin> \<pp>
 8. g \<notin> \<pp>
[PROOF STEP]
qed (use HU in auto)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zariski_open U
\<pp> \<in> U
s' \<in> \<O> U
t' \<in> \<O> U
s = st.class_of U s'
t = st.class_of U t'
s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)
t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
a \<in> R
b \<in> R
f \<in> R
g \<in> R
f \<notin> \<pp>
g \<notin> \<pp>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence fact:"local.frac a f = local.frac b g"
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
\<pp> \<in> U
s' \<in> \<O> U
t' \<in> \<O> U
s = st.class_of U s'
t = st.class_of U t'
s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)
t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
a \<in> R
b \<in> R
f \<in> R
g \<in> R
f \<notin> \<pp>
g \<notin> \<pp>

goal (1 subgoal):
 1. local.frac a f = local.frac b g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "local.frac a f = key_map U s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.frac a f = local.key_map U s'
[PROOF STEP]
using key_map_def \<open>\<pp> \<in> U\<close> \<open>s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)\<close> \<open>s' \<in> \<O> U\<close>
[PROOF STATE]
proof (prove)
using this:
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
\<pp> \<in> U
s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f)
s' \<in> \<O> U

goal (1 subgoal):
 1. local.frac a f = local.key_map U s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.frac a f = local.key_map U s'

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.frac a f = local.key_map U s'

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> (st.canonical_fun U s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.key_map U s' = \<phi> (st.canonical_fun U s')
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> \<open>is_zariski_open U\<close> \<open>s' \<in> \<O> U\<close> assms(4) pr.presheaf_of_rings_axioms top.neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
is_zariski_open U
s' \<in> \<O> U
\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s
presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}

goal (1 subgoal):
 1. local.key_map U s' = \<phi> (st.canonical_fun U s')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
local.key_map U s' = \<phi> (st.canonical_fun U s')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.key_map U s' = \<phi> (st.canonical_fun U s')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> (st.class_of U s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.canonical_fun U s') = \<phi> (st.class_of U s')
[PROOF STEP]
using direct_lim.canonical_fun_def is_prime st.canonical_fun_def st.class_of_def
[PROOF STATE]
proof (prove)
using this:
direct_lim ?S ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?I \<Longrightarrow> direct_lim.canonical_fun ?\<FF> ?\<rho> ?I ?U ?x = direct_lim.class_of ?\<FF> ?\<rho> ?I ?U ?x
\<pp> \<in> Spec
st.canonical_fun ?U ?x = st.class_of ?U ?x
st.class_of ?U ?s \<equiv> equivalence.Class (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y} (?U, ?s)

goal (1 subgoal):
 1. \<phi> (st.canonical_fun U s') = \<phi> (st.class_of U s')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun U s') = \<phi> (st.class_of U s')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun U s') = \<phi> (st.class_of U s')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.class_of U s') = \<phi> s
[PROOF STEP]
by (simp add: \<open>s = st.class_of U s'\<close>)
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of U s') = \<phi> s

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of U s') = \<phi> s

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s = \<phi> t
[PROOF STEP]
using \<open>\<phi> s = \<phi> t\<close>
[PROOF STATE]
proof (prove)
using this:
\<phi> s = \<phi> t

goal (1 subgoal):
 1. \<phi> s = \<phi> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> s = \<phi> t

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> s = \<phi> t

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> (st.class_of U t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> t = \<phi> (st.class_of U t')
[PROOF STEP]
using \<open>t = st.class_of U t'\<close>
[PROOF STATE]
proof (prove)
using this:
t = st.class_of U t'

goal (1 subgoal):
 1. \<phi> t = \<phi> (st.class_of U t')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> t = \<phi> (st.class_of U t')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> t = \<phi> (st.class_of U t')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = \<phi> (st.canonical_fun U t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.class_of U t') = \<phi> (st.canonical_fun U t')
[PROOF STEP]
using direct_lim.canonical_fun_def is_prime st.canonical_fun_def st.class_of_def
[PROOF STATE]
proof (prove)
using this:
direct_lim ?S ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?I \<Longrightarrow> direct_lim.canonical_fun ?\<FF> ?\<rho> ?I ?U ?x = direct_lim.class_of ?\<FF> ?\<rho> ?I ?U ?x
\<pp> \<in> Spec
st.canonical_fun ?U ?x = st.class_of ?U ?x
st.class_of ?U ?s \<equiv> equivalence.Class (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y} (?U, ?s)

goal (1 subgoal):
 1. \<phi> (st.class_of U t') = \<phi> (st.canonical_fun U t')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of U t') = \<phi> (st.canonical_fun U t')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of U t') = \<phi> (st.canonical_fun U t')

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = key_map U t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.canonical_fun U t') = local.key_map U t'
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> \<open>is_zariski_open U\<close> \<open>t' \<in> \<O> U\<close> assms(4) top.neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
is_zariski_open U
t' \<in> \<O> U
\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}

goal (1 subgoal):
 1. \<phi> (st.canonical_fun U t') = local.key_map U t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun U t') = local.key_map U t'

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun U t') = local.key_map U t'

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
have "\<dots> = local.frac b g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.key_map U t' = local.frac b g
[PROOF STEP]
using FU(4) local.key_map_def t'
[PROOF STATE]
proof (prove)
using this:
t' \<in> \<O> U
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)

goal (1 subgoal):
 1. local.key_map U t' = local.frac b g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
local.key_map U t' = local.frac b g

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; t' \<in> \<O> U; s = st.class_of U s'; t = st.class_of U t'; s' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f); t' = (\<lambda>\<qq>\<in>U. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g); a \<in> R; b \<in> R; f \<in> R; g \<in> R; f \<notin> \<pp>; g \<notin> \<pp>\<rbrakk> \<Longrightarrow> local.frac a f = local.frac b g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.frac a f = local.frac b g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.frac a f = local.frac b g

goal (1 subgoal):
 1. local.frac a f = local.frac b g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.frac a f = local.frac b g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.frac a f = local.frac b g

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.frac a f = local.frac b g
[PROOF STEP]
obtain h where Hh: "h \<in> R" "h \<notin> \<pp>" "h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
local.frac a f = local.frac b g

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> R; h \<notin> \<pp>; h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pi.eq_from_eq_frac
[PROOF STATE]
proof (prove)
using this:
local.frac a f = local.frac b g
\<lbrakk>local.frac ?r ?s = local.frac ?r' ?s'; ?s \<in> R\<setminus>\<pp>; ?s' \<in> R\<setminus>\<pp>; ?r \<in> R; ?r' \<in> R; \<And>h. \<lbrakk>h \<in> R\<setminus>\<pp>; h \<cdot> (?s' \<cdot> ?r - ?s \<cdot> ?r') = \<zero>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> R; h \<notin> \<pp>; h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Diff_iff \<open>a \<in> R\<close> \<open>b \<in> R\<close> \<open>f \<in> R\<close> \<open>f \<notin> \<pp>\<close> \<open>g \<in> R\<close> \<open>g \<notin> \<pp>\<close>)
[PROOF STATE]
proof (state)
this:
h \<in> R
h \<notin> \<pp>
h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have izo: "is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
[PROOF STEP]
using local.standard_open_is_zariski_open
[PROOF STATE]
proof (prove)
using this:
?x \<in> local.carrier_quotient_ring \<Longrightarrow> local.local.is_zariski_open (local.local.standard_open ?x)

goal (1 subgoal):
 1. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
[PROOF STEP]
by (simp add: Hh(1) \<open>f \<in> R\<close> \<open>g \<in> R\<close> standard_open_is_zariski_open)
[PROOF STATE]
proof (state)
this:
is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have ssm_s': "sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s'
                \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
[PROOF STEP]
by (metis (no_types, opaque_lifting) FU(3) Int_assoc inf_le1 izo map.map_closed sheaf_spec_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have ssm_t': "sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t'
                \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
[PROOF STEP]
by (metis (no_types, opaque_lifting) FU(4) Int_assoc inf_le1 izo map.map_closed sheaf_spec_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have [simp]: "\<pp> \<in> \<D>(f)" "\<pp> \<in> \<D>(g)" "\<pp> \<in> \<D>(h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> \<D>(f) &&& \<pp> \<in> \<D>(g) &&& \<pp> \<in> \<D>(h)
[PROOF STEP]
using Hh \<open>f \<in> R\<close> \<open>f \<notin> \<pp>\<close> \<open>g \<in> R\<close> \<open>g \<notin> \<pp>\<close> belongs_standard_open_iff st.is_elem
[PROOF STATE]
proof (prove)
using this:
h \<in> R
h \<notin> \<pp>
h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>
f \<in> R
f \<notin> \<pp>
g \<in> R
g \<notin> \<pp>
\<lbrakk>?x \<in> R; ?\<pp> \<in> Spec\<rbrakk> \<Longrightarrow> (?x \<notin> ?\<pp>) = (?\<pp> \<in> \<D>(?x))
\<pp> \<in> Spec

goal (1 subgoal):
 1. \<pp> \<in> \<D>(f) &&& \<pp> \<in> \<D>(g) &&& \<pp> \<in> \<D>(h)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<pp> \<in> \<D>(f)
\<pp> \<in> \<D>(g)
\<pp> \<in> \<D>(h)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have eq: "s' \<qq> = t' \<qq>" if "\<qq> \<in> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
have "\<qq> \<in> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<qq> \<in> Spec
[PROOF STEP]
using standard_open_def that
[PROOF STATE]
proof (prove)
using this:
\<D>(?x) \<equiv> Spec\<setminus>\<V> \<langle>?x\<rangle>
\<qq> \<in> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)

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

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<qq> \<in> Spec
[PROOF STEP]
interpret q: quotient_ring "R\<setminus>\<qq>" R "(+)" "(\<cdot>)" \<zero>
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> Spec

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using spectrum_imp_cxt_quotient_ring
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> Spec
?\<pp> \<in> Spec \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
note local.q.sub [simp del]  \<comment>\<open>Because it definitely loops\<close>
[PROOF STATE]
proof (state)
this:
?a \<in> R\<setminus>\<qq> \<Longrightarrow> ?a \<in> R

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
define RR where "RR \<equiv> {(x, y). (x, y) \<in> (R \<times> (R\<setminus>\<qq>)) \<times> R \<times> (R\<setminus>\<qq>) \<and> q.rel x y}"
[PROOF STATE]
proof (state)
this:
RR \<equiv> {(x, y). (x, y) \<in> (R \<times> (R\<setminus>\<qq>)) \<times> R \<times> (R\<setminus>\<qq>) \<and> q.rel x y}

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
interpret eq: equivalence "R \<times> (R\<setminus>\<qq>)" "RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (R \<times> (R\<setminus>\<qq>)) RR
[PROOF STEP]
unfolding RR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (R \<times> (R\<setminus>\<qq>)) {(x, y). (x, y) \<in> (R \<times> (R\<setminus>\<qq>)) \<times> R \<times> (R\<setminus>\<qq>) \<and> q.rel x y}
[PROOF STEP]
by (blast intro: equivalence.intro q.rel_refl q.rel_sym q.rel_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
have Fq [simp]: "f \<notin> \<qq>" "g \<notin> \<qq>" "h \<notin> \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<notin> \<qq> &&& g \<notin> \<qq> &&& h \<notin> \<qq>
[PROOF STEP]
using belongs_standard_open_iff that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> R; ?\<pp> \<in> Spec\<rbrakk> \<Longrightarrow> (?x \<notin> ?\<pp>) = (?\<pp> \<in> \<D>(?x))
\<qq> \<in> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)

goal (1 subgoal):
 1. f \<notin> \<qq> &&& g \<notin> \<qq> &&& h \<notin> \<qq>
[PROOF STEP]
apply (meson Int_iff \<open>\<qq> \<in> Spec\<close> \<open>f \<in> R\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g \<notin> \<qq>
 2. h \<notin> \<qq>
[PROOF STEP]
apply (meson Int_iff \<open>\<qq> \<in> Spec\<close> \<open>g \<in> R\<close> belongs_standard_open_iff that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<notin> \<qq>
[PROOF STEP]
by (meson Hh(1) IntD2 \<open>\<qq> \<in> Spec\<close> belongs_standard_open_iff that)
[PROOF STATE]
proof (state)
this:
f \<notin> \<qq>
g \<notin> \<qq>
h \<notin> \<qq>

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<notin> \<qq>
g \<notin> \<qq>
h \<notin> \<qq>

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
have "eq.Class (a, f) = eq.Class (b, g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq.Class (a, f) = eq.Class (b, g)
[PROOF STEP]
proof (rule eq.Class_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((a, f), b, g) \<in> RR
[PROOF STEP]
have "\<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>
[PROOF STEP]
using Hh \<open>h \<notin> \<qq>\<close>
[PROOF STATE]
proof (prove)
using this:
h \<in> R
h \<notin> \<pp>
h \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>
h \<notin> \<qq>

goal (1 subgoal):
 1. \<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>

goal (1 subgoal):
 1. ((a, f), b, g) \<in> RR
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>
[PROOF STEP]
show "((a,f), b,g) \<in> RR"
[PROOF STATE]
proof (prove)
using this:
\<exists>s1. s1 \<in> R \<and> s1 \<notin> \<qq> \<and> s1 \<cdot> (g \<cdot> a - f \<cdot> b) = \<zero>

goal (1 subgoal):
 1. ((a, f), b, g) \<in> RR
[PROOF STEP]
by (simp add: RR_def q.rel_def  \<open>a \<in> R\<close> \<open>b \<in> R\<close> \<open>f \<in> R\<close> \<open>g \<in> R\<close>)
[PROOF STATE]
proof (state)
this:
((a, f), b, g) \<in> RR

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eq.Class (a, f) = eq.Class (b, g)

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<notin> \<qq>
g \<notin> \<qq>
h \<notin> \<qq>
eq.Class (a, f) = eq.Class (b, g)
[PROOF STEP]
have "q.frac a f = q.frac b g"
[PROOF STATE]
proof (prove)
using this:
f \<notin> \<qq>
g \<notin> \<qq>
h \<notin> \<qq>
eq.Class (a, f) = eq.Class (b, g)

goal (1 subgoal):
 1. q.frac a f = q.frac b g
[PROOF STEP]
using RR_def q.frac_def
[PROOF STATE]
proof (prove)
using this:
f \<notin> \<qq>
g \<notin> \<qq>
h \<notin> \<qq>
eq.Class (a, f) = eq.Class (b, g)
RR \<equiv> {(x, y). (x, y) \<in> (R \<times> (R\<setminus>\<qq>)) \<times> R \<times> (R\<setminus>\<qq>) \<and> q.rel x y}
q.frac ?r ?s \<equiv> equivalence.Class (R \<times> (R\<setminus>\<qq>)) {(x, y). (x, y) \<in> (R \<times> (R\<setminus>\<qq>)) \<times> R \<times> (R\<setminus>\<qq>) \<and> q.rel x y} (?r, ?s)

goal (1 subgoal):
 1. q.frac a f = q.frac b g
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
q.frac a f = q.frac b g

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
thus "s' \<qq> = t' \<qq>"
[PROOF STATE]
proof (prove)
using this:
q.frac a f = q.frac b g

goal (1 subgoal):
 1. s' \<qq> = t' \<qq>
[PROOF STEP]
by (simp add: s' t')
[PROOF STATE]
proof (state)
this:
s' \<qq> = t' \<qq>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<Longrightarrow> s' ?\<qq>3 = t' ?\<qq>3

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> st.carrier_stalk; y \<in> st.carrier_stalk; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
have "s = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s')
[PROOF STEP]
using \<open>\<pp> \<in> \<D>(f)\<close> \<open>\<pp> \<in> \<D>(g)\<close> \<open>\<pp> \<in> \<D>(h)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> \<D>(f)
\<pp> \<in> \<D>(g)
\<pp> \<in> \<D>(h)

goal (1 subgoal):
 1. s = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s')
[PROOF STEP]
by (smt (verit, ccfv_threshold) FU(1-3) IntE IntI izo s(1) same_class_from_restrict subsetI)
[PROOF STATE]
proof (state)
this:
s = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s')

goal (1 subgoal):
 1. s = t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s')

goal (1 subgoal):
 1. s = t
[PROOF STEP]
have "\<dots> = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
[PROOF STEP]
proof (rule local.st.class_of_eqI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h), sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') \<in> Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec
 2. (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h), sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t') \<in> Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec
 3. ?W \<in> {U. is_zariski_open U \<and> \<pp> \<in> U}
 4. ?W \<subseteq> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<inter> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 5. sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) ?W (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) ?W (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
[PROOF STEP]
show "sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
[PROOF STEP]
proof (rule local.pr.eq_\<rho>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 2. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 3. is_zariski_open ?W
 4. ?W \<subseteq> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<inter> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 5. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 6. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 7. sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) ?W (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) ?W (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
 8. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 9. U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<subseteq> ?W
[PROOF STEP]
show "sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') =
                  sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
[PROOF STEP]
using eq FU(3) FU(4)
[PROOF STATE]
proof (prove)
using this:
?\<qq>3 \<in> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<Longrightarrow> s' ?\<qq>3 = t' ?\<qq>3
s' \<in> \<O> U
t' \<in> \<O> U

goal (1 subgoal):
 1. sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')
[PROOF STEP]
apply (simp add: sheaf_spec_morphisms_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<qq>. \<qq> \<in> U \<and> \<qq> \<in> \<D>(f) \<and> \<qq> \<in> \<D>(g) \<and> \<qq> \<in> \<D>(h) \<Longrightarrow> s' \<qq> = t' \<qq>) \<Longrightarrow> (restrict s' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<longrightarrow> (restrict t' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<longrightarrow> restrict s' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) = restrict t' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))) \<and> (restrict t' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<notin> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<longrightarrow> restrict s' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) = undefined)) \<and> (restrict s' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<notin> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<longrightarrow> restrict t' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) \<longrightarrow> undefined = restrict t' (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)))
[PROOF STEP]
apply (metis eq restrict_ext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')

goal (8 subgoals):
 1. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 2. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 3. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 4. U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<subseteq> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<inter> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 5. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 6. sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t' \<in> \<O> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 7. is_zariski_open (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
 8. U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<subseteq> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)
[PROOF STEP]
qed (use izo ssm_s' ssm_t' in auto)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = sheaf_spec_morphisms (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')

goal (4 subgoals):
 1. (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h), sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') \<in> Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec
 2. (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h), sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t') \<in> Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec
 3. U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<in> {U. is_zariski_open U \<and> \<pp> \<in> U}
 4. U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<subseteq> U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h) \<inter> (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h))
[PROOF STEP]
qed (auto simp: izo ssm_s' ssm_t')
[PROOF STATE]
proof (state)
this:
st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')

goal (1 subgoal):
 1. s = t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) s') = st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t')

goal (1 subgoal):
 1. s = t
[PROOF STEP]
have "\<dots> = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t') = t
[PROOF STEP]
using \<open>\<pp> \<in> \<D>(f)\<close> \<open>\<pp> \<in> \<D>(g)\<close> \<open>\<pp> \<in> \<D>(h)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> \<D>(f)
\<pp> \<in> \<D>(g)
\<pp> \<in> \<D>(h)

goal (1 subgoal):
 1. st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t') = t
[PROOF STEP]
by (smt (verit, ccfv_threshold) FU(1-4) IntE IntI izo s(2) same_class_from_restrict subsetI)
[PROOF STATE]
proof (state)
this:
st.class_of (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) (sheaf_spec_morphisms U (U \<inter> \<D>(f) \<inter> \<D>(g) \<inter> \<D>(h)) t') = t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
s = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
s = t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on \<phi> st.carrier_stalk

goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on \<phi> st.carrier_stalk

goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
have "\<phi> ` st.carrier_stalk = (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` st.carrier_stalk = pi.carrier_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> ` st.carrier_stalk \<subseteq> pi.carrier_local_ring_at
 2. pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk
[PROOF STEP]
show "\<phi> ` st.carrier_stalk \<subseteq> pi.carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` st.carrier_stalk \<subseteq> pi.carrier_local_ring_at
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. \<phi> ` st.carrier_stalk \<subseteq> pi.carrier_local_ring_at
[PROOF STEP]
by (simp add: image_subset_of_target ring_homomorphism_def)
[PROOF STATE]
proof (state)
this:
\<phi> ` st.carrier_stalk \<subseteq> pi.carrier_local_ring_at

goal (1 subgoal):
 1. pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk
[PROOF STEP]
show "pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
assume H:"x \<in> (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (state)
this:
x \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
obtain a f where F:"a \<in> R" "f \<in> R" "f \<notin> \<pp>" "x = local.frac a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a f. \<lbrakk>a \<in> R; f \<in> R; f \<notin> \<pp>; x = local.frac a f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pi.frac_from_carrier_local H
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> pi.carrier_local_ring_at; \<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> \<pp>; ?X = local.frac r s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
x \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. (\<And>a f. \<lbrakk>a \<in> R; f \<in> R; f \<notin> \<pp>; x = local.frac a f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> R
f \<in> R
f \<notin> \<pp>
x = local.frac a f

goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
define s where sec_def:"s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f"
[PROOF STATE]
proof (state)
this:
s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f

goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f
[PROOF STEP]
have sec:"s \<in> \<O>(\<D>(f))"
[PROOF STATE]
proof (prove)
using this:
s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
have "s \<qq> \<in> (R\<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>)" if "\<qq> \<in> \<D>(f)" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
have "f \<notin> \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<notin> \<qq>
[PROOF STEP]
using that belongs_standard_open_iff F(2) standard_open_is_subset
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> \<D>(f)
\<lbrakk>?x \<in> R; ?\<pp> \<in> Spec\<rbrakk> \<Longrightarrow> (?x \<notin> ?\<pp>) = (?\<pp> \<in> \<D>(?x))
f \<in> R
?x \<in> R \<Longrightarrow> \<D>(?x) \<subseteq> Spec

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

goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<notin> \<qq>
[PROOF STEP]
have "quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> (R\<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
f \<notin> \<qq>

goal (1 subgoal):
 1. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
using F(1,2) frac_in_carrier_local \<open>\<qq> \<in> \<D>(f)\<close> standard_open_is_subset
[PROOF STATE]
proof (prove)
using this:
f \<notin> \<qq>
a \<in> R
f \<in> R
\<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>
\<qq> \<in> \<D>(f)
?x \<in> R \<Longrightarrow> \<D>(?x) \<subseteq> Spec

goal (1 subgoal):
 1. quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
thus "s \<qq> \<in> (R\<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
using sec_def
[PROOF STATE]
proof (prove)
using this:
quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f

goal (1 subgoal):
 1. s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
by (simp add: \<open>\<qq> \<in> \<D>(f)\<close>)
[PROOF STATE]
proof (state)
this:
s \<qq> \<in> R \<^bsub>\<qq> (+) (\<cdot>) \<zero>\<^esub>

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

goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> \<D>(f) \<Longrightarrow> s ?\<qq>3 \<in> R \<^bsub>?\<qq>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
have "s \<in>  extensional (\<D>(f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> extensional \<D>(f)
[PROOF STEP]
using sec_def
[PROOF STATE]
proof (prove)
using this:
s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f

goal (1 subgoal):
 1. s \<in> extensional \<D>(f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> extensional \<D>(f)

goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<in> extensional \<D>(f)

goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
have "is_regular s \<D>(f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular s \<D>(f)
[PROOF STEP]
using F(1,2) standard_open_is_subset  belongs_standard_open_iff is_regular_def[of s "\<D>(f)"] standard_open_is_zariski_open
[PROOF STATE]
proof (prove)
using this:
a \<in> R
f \<in> R
?x \<in> R \<Longrightarrow> \<D>(?x) \<subseteq> Spec
\<lbrakk>?x \<in> R; ?\<pp> \<in> Spec\<rbrakk> \<Longrightarrow> (?x \<notin> ?\<pp>) = (?\<pp> \<in> \<D>(?x))
is_regular s \<D>(f) \<equiv> \<forall>\<pp>. \<pp> \<in> \<D>(f) \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> \<D>(f) \<and> \<pp> \<in> V \<and> is_locally_frac s V)
?x \<in> R \<Longrightarrow> is_zariski_open \<D>(?x)

goal (1 subgoal):
 1. is_regular s \<D>(f)
[PROOF STEP]
by (smt is_locally_frac_def restrict_apply sec_def subsetD subsetI)
[PROOF STATE]
proof (state)
this:
is_regular s \<D>(f)

goal (1 subgoal):
 1. s \<equiv> \<lambda>\<qq>\<in>\<D>(f). quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f \<Longrightarrow> s \<in> \<O> \<D>(f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<qq>3 \<in> \<D>(f) \<Longrightarrow> s ?\<qq>3 \<in> R \<^bsub>?\<qq>3 (+) (\<cdot>) \<zero>\<^esub>
s \<in> extensional \<D>(f)
is_regular s \<D>(f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<qq>3 \<in> \<D>(f) \<Longrightarrow> s ?\<qq>3 \<in> R \<^bsub>?\<qq>3 (+) (\<cdot>) \<zero>\<^esub>
s \<in> extensional \<D>(f)
is_regular s \<D>(f)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<O> \<D>(f)
[PROOF STEP]
have im:"\<phi> (st.class_of \<D>(f) s) = local.frac a f"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
have "\<phi> (st.class_of \<D>(f) s) = \<phi> (st.canonical_fun \<D>(f) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = \<phi> (st.canonical_fun \<D>(f) s)
[PROOF STEP]
using st.canonical_fun_def direct_lim.canonical_fun_def st.class_of_def is_prime
[PROOF STATE]
proof (prove)
using this:
st.canonical_fun ?U ?x = st.class_of ?U ?x
direct_lim ?S ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?I \<Longrightarrow> direct_lim.canonical_fun ?\<FF> ?\<rho> ?I ?U ?x = direct_lim.class_of ?\<FF> ?\<rho> ?I ?U ?x
st.class_of ?U ?s \<equiv> equivalence.Class (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y} (?U, ?s)
\<pp> \<in> Spec

goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = \<phi> (st.canonical_fun \<D>(f) s)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of \<D>(f) s) = \<phi> (st.canonical_fun \<D>(f) s)

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of \<D>(f) s) = \<phi> (st.canonical_fun \<D>(f) s)

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
have "\<dots> = key_map \<D>(f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (st.canonical_fun \<D>(f) s) = local.key_map \<D>(f) s
[PROOF STEP]
using all_eq st.is_elem F(2) F(3) sec
[PROOF STATE]
proof (prove)
using this:
\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s
\<pp> \<in> Spec
f \<in> R
f \<notin> \<pp>
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. \<phi> (st.canonical_fun \<D>(f) s) = local.key_map \<D>(f) s
[PROOF STEP]
apply (simp add: top.neighborhoods_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>U. is_zariski_open U \<and> \<pp> \<in> U \<longrightarrow> (\<forall>s\<in>\<O> U. \<phi> (st.canonical_fun U s) = local.key_map U s); \<pp> \<in> Spec; f \<in> R; f \<notin> \<pp>; s \<in> \<O> \<D>(f)\<rbrakk> \<Longrightarrow> \<phi> (st.canonical_fun \<D>(f) s) = local.key_map \<D>(f) s
[PROOF STEP]
by (meson belongs_standard_open_iff standard_open_is_zariski_open)
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun \<D>(f) s) = local.key_map \<D>(f) s

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (st.canonical_fun \<D>(f) s) = local.key_map \<D>(f) s

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
have "... = local.frac a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.key_map \<D>(f) s = local.frac a f
[PROOF STEP]
by (metis (mono_tags, lifting) F(2,3) belongs_standard_open_iff is_prime key_map_def restrict_apply sec sec_def)
[PROOF STATE]
proof (state)
this:
local.key_map \<D>(f) s = local.frac a f

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f) \<Longrightarrow> \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (st.class_of \<D>(f) s) = local.frac a f

goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = local.frac a f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of \<D>(f) s) = local.frac a f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> (st.class_of \<D>(f) s) = local.frac a f

goal (1 subgoal):
 1. \<And>x. x \<in> pi.carrier_local_ring_at \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
thus "x \<in> \<phi> ` st.carrier_stalk"
[PROOF STATE]
proof (prove)
using this:
\<phi> (st.class_of \<D>(f) s) = local.frac a f

goal (1 subgoal):
 1. x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = local.frac a f \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
have "st.class_of \<D>(f) s \<in> st.carrier_stalk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
have "\<pp> \<in> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
using is_prime
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> Spec

goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pp> \<in> Spec

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pp> \<in> Spec

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
have "\<D>(f) \<in> (top.neighborhoods \<pp>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>(f) \<in> top.neighborhoods \<pp>
[PROOF STEP]
using top.neighborhoods_def belongs_standard_open_iff F(2,3) is_prime standard_open_is_zariski_open standard_open_is_subset
[PROOF STATE]
proof (prove)
using this:
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}
\<lbrakk>?x \<in> R; ?\<pp> \<in> Spec\<rbrakk> \<Longrightarrow> (?x \<notin> ?\<pp>) = (?\<pp> \<in> \<D>(?x))
f \<in> R
f \<notin> \<pp>
\<pp> \<in> Spec
?x \<in> R \<Longrightarrow> is_zariski_open \<D>(?x)
?x \<in> R \<Longrightarrow> \<D>(?x) \<subseteq> Spec

goal (1 subgoal):
 1. \<D>(f) \<in> top.neighborhoods \<pp>
[PROOF STEP]
by (metis (no_types, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<D>(f) \<in> top.neighborhoods \<pp>

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<D>(f) \<in> top.neighborhoods \<pp>

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
have "s \<in> \<O> \<D>(f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> \<O> \<D>(f)
[PROOF STEP]
using sec
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. s \<in> \<O> \<D>(f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pp> \<in> Spec
\<D>(f) \<in> top.neighborhoods \<pp>
s \<in> \<O> \<D>(f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> Spec
\<D>(f) \<in> top.neighborhoods \<pp>
s \<in> \<O> \<D>(f)

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
using st.class_of_in_stalk
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> Spec
\<D>(f) \<in> top.neighborhoods \<pp>
s \<in> \<O> \<D>(f)
\<lbrakk>?A \<in> top.neighborhoods \<pp>; ?z \<in> \<O> ?A\<rbrakk> \<Longrightarrow> st.class_of ?A ?z \<in> st.carrier_stalk

goal (1 subgoal):
 1. st.class_of \<D>(f) s \<in> st.carrier_stalk
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st.class_of \<D>(f) s \<in> st.carrier_stalk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
st.class_of \<D>(f) s \<in> st.carrier_stalk

goal (1 subgoal):
 1. \<phi> (st.class_of \<D>(f) s) = local.frac a f \<Longrightarrow> x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
st.class_of \<D>(f) s \<in> st.carrier_stalk

goal (1 subgoal):
 1. x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
using F(4) im
[PROOF STATE]
proof (prove)
using this:
st.class_of \<D>(f) s \<in> st.carrier_stalk
x = local.frac a f
\<phi> (st.class_of \<D>(f) s) = local.frac a f

goal (1 subgoal):
 1. x \<in> \<phi> ` st.carrier_stalk
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<phi> ` st.carrier_stalk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> \<phi> ` st.carrier_stalk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pi.carrier_local_ring_at \<subseteq> \<phi> ` st.carrier_stalk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> ` st.carrier_stalk = pi.carrier_local_ring_at

goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on \<phi> st.carrier_stalk
\<phi> ` st.carrier_stalk = pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on \<phi> st.carrier_stalk
\<phi> ` st.carrier_stalk = pi.carrier_local_ring_at

goal (1 subgoal):
 1. bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at
[PROOF STEP]
by (simp add: bij_betw_def)
[PROOF STATE]
proof (state)
this:
bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bij_betw \<phi> st.carrier_stalk pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stalk_at_prime_is_iso_to_local_ring_at_prime:
  assumes "is_zariski_open V" and "\<pp> \<in> V"
  shows "\<exists>\<phi>. ring_isomorphism \<phi>
st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. ring_isomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
using key_ring_morphism stalk_at_prime_is_iso_to_local_ring_at_prime_aux assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_zariski_open ?V; \<pp> \<in> ?V\<rbrakk> \<Longrightarrow> \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk ?V) (st.one_stalk ?V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
\<lbrakk>is_zariski_open ?V; \<pp> \<in> ?V; ring_homomorphism ?\<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk ?V) (st.one_stalk ?V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at; \<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (?\<phi> \<circ> st.canonical_fun U) s = local.key_map U s\<rbrakk> \<Longrightarrow> ring_isomorphism ?\<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk ?V) (st.one_stalk ?V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
is_zariski_open V
\<pp> \<in> V

goal (1 subgoal):
 1. \<exists>\<phi>. ring_isomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
by meson


[STATEMENT]
lemma spec_is_locally_ringed_space:
  shows "locally_ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b
add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locally_ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
proof (intro locally_ringed_space.intro locally_ringed_space_axioms.intro)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
 2. \<And>x U. \<lbrakk>x \<in> U; is_zariski_open U\<rbrakk> \<Longrightarrow> stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods x) x U
[PROOF STEP]
interpret sh: sheaf_of_rings Spec is_zariski_open sheaf_spec
     sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec
     zero_sheaf_spec one_sheaf_spec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
using sheaf_spec_is_sheaf
[PROOF STATE]
proof (prove)
using this:
sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
 2. \<And>x U. \<lbrakk>x \<in> U; is_zariski_open U\<rbrakk> \<Longrightarrow> stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods x) x U
[PROOF STEP]
show "ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
using spec_is_ringed_space
[PROOF STATE]
proof (prove)
using this:
ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. \<And>x U. \<lbrakk>x \<in> U; is_zariski_open U\<rbrakk> \<Longrightarrow> stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods x) x U
[PROOF STEP]
show "stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec
zero_sheaf_spec one_sheaf_spec (pr.neighborhoods \<pp>) \<pp> U"
    if "\<pp> \<in> U" "is_zariski_open U" for \<pp> U
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods \<pp>) \<pp> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods \<pp>) \<pp> U
[PROOF STEP]
interpret st: stalk Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec
      mult_sheaf_spec zero_sheaf_spec one_sheaf_spec "pr.neighborhoods \<pp>" \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stalk Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods \<pp>) \<pp>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>U. U \<in> pr.neighborhoods \<pp> \<Longrightarrow> is_zariski_open U
 2. \<And>U V. \<lbrakk>U \<in> pr.neighborhoods \<pp>; V \<in> pr.neighborhoods \<pp>\<rbrakk> \<Longrightarrow> \<exists>W\<in>pr.neighborhoods \<pp>. W \<subseteq> U \<inter> V
 3. \<pp> \<in> Spec
 4. pr.neighborhoods \<pp> = {U. is_zariski_open U \<and> \<pp> \<in> U}
[PROOF STEP]
show "\<pp> \<in> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
by (meson in_mono that zariski_open_is_subset)
[PROOF STATE]
proof (state)
this:
\<pp> \<in> Spec

goal (3 subgoals):
 1. \<And>U. U \<in> pr.neighborhoods \<pp> \<Longrightarrow> is_zariski_open U
 2. \<And>U V. \<lbrakk>U \<in> pr.neighborhoods \<pp>; V \<in> pr.neighborhoods \<pp>\<rbrakk> \<Longrightarrow> \<exists>W\<in>pr.neighborhoods \<pp>. W \<subseteq> U \<inter> V
 3. pr.neighborhoods \<pp> = {U. is_zariski_open U \<and> \<pp> \<in> U}
[PROOF STEP]
qed (auto simp: pr.neighborhoods_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
interpret pri: 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 (simp add: spectrum_imp_pr st.is_elem)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
interpret km: key_map R "(+)" "(\<cdot>)" \<zero> \<one> \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key_map R (+) (\<cdot>) \<zero> \<one> \<pp>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
qed (simp add: st.is_elem)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
have "ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
[PROOF STEP]
using st.stalk_is_ring sheaf_spec_is_presheaf \<open>is_zariski_open U\<close> \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_zariski_open ?V; \<pp> \<in> ?V\<rbrakk> \<Longrightarrow> ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk ?V) (st.one_stalk ?V)
presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
is_zariski_open U
\<pp> \<in> U

goal (1 subgoal):
 1. ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
have "local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at
                 pri.zero_local_ring_at pri.one_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
[PROOF STEP]
using pr_ideal.local_ring_at_is_local
[PROOF STATE]
proof (prove)
using this:
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> local_ring ?R \<^bsub>?I ?addition ?multiplication ?zero\<^esub> (pr_ideal.add_local_ring_at ?R ?I ?addition ?multiplication ?zero) (pr_ideal.mult_local_ring_at ?R ?I ?addition ?multiplication ?zero) (pr_ideal.zero_local_ring_at ?R ?I ?addition ?multiplication ?zero ?unit) (pr_ideal.one_local_ring_at ?R ?I ?addition ?multiplication ?zero ?unit)

goal (1 subgoal):
 1. local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
[PROOF STEP]
by (simp add: pr_ideal.local_ring_at_is_local spectrum_imp_pr st.is_elem)
[PROOF STATE]
proof (state)
this:
local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
note st.subset_of_opens [simp del]
[PROOF STATE]
proof (state)
this:
?U \<in> pr.neighborhoods \<pp> \<Longrightarrow> is_zariski_open ?U

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
have "\<exists>f. ring_isomorphism f
st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pr_ideal.add_local_ring_at R \<pp> (+) (\<cdot>) \<zero>) (pr_ideal.mult_local_ring_at R \<pp> (+) (\<cdot>) \<zero>) (pr_ideal.zero_local_ring_at R \<pp> (+) (\<cdot>) \<zero> \<one>) (pr_ideal.one_local_ring_at R \<pp> (+) (\<cdot>) \<zero> \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. ring_isomorphism f st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U) pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
[PROOF STEP]
by (simp add: km.stalk_at_prime_is_iso_to_local_ring_at_prime st.index that)
[PROOF STATE]
proof (state)
this:
\<exists>f. ring_isomorphism f st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U) pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
\<exists>f. ring_isomorphism f st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U) pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
[PROOF STEP]
show "stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec
zero_sheaf_spec one_sheaf_spec (pr.neighborhoods \<pp>) \<pp> U"
[PROOF STATE]
proof (prove)
using this:
ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
\<exists>f. ring_isomorphism f st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U) pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
using isomorphic_to_local_is_local \<open>\<pp> \<in> U\<close> \<open>is_zariski_open U\<close> st.is_local_def
[PROOF STATE]
proof (prove)
using this:
ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U)
local_ring pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
\<exists>f. ring_isomorphism f st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk U) (st.one_stalk U) pri.carrier_local_ring_at pri.add_local_ring_at pri.mult_local_ring_at pri.zero_local_ring_at pri.one_local_ring_at
\<lbrakk>local_ring ?B ?addB ?multB ?zeroB ?oneB; ring_isomorphism ?f ?A ?addA ?multA ?zeroA ?oneA ?B ?addB ?multB ?zeroB ?oneB\<rbrakk> \<Longrightarrow> local_ring ?A ?addA ?multA ?zeroA ?oneA
\<pp> \<in> U
is_zariski_open U
st.is_local ?U \<equiv> local_ring st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk ?U) (st.one_stalk ?U)

goal (1 subgoal):
 1. st.is_local U
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
st.is_local U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<pp>3 \<in> ?U3; is_zariski_open ?U3\<rbrakk> \<Longrightarrow> stalk.is_local is_zariski_open sheaf_spec sheaf_spec_morphisms add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (pr.neighborhoods ?\<pp>3) ?\<pp>3 ?U3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_in_O:
  assumes "is_open\<^sub>Y V" "q \<in> \<O>\<^sub>Y V"
  shows "\<phi>\<^sub>f V q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X (V))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sub>f V q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X V)
[PROOF STEP]
using is_morphism_of_sheaves morphism_presheaves_of_rings.fam_morphisms_are_maps
[PROOF STATE]
proof (prove)
using this:
morphism_sheaves_of_rings Y is_open\<^sub>Y \<O>\<^sub>Y \<rho>\<^sub>Y d add_str\<^sub>Y mult_str\<^sub>Y zero_str\<^sub>Y one_str\<^sub>Y local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<phi>\<^sub>f
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (?fam_morphisms ?U) (?\<FF> ?U) (?\<FF>' ?U)

goal (1 subgoal):
 1. \<phi>\<^sub>f V q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X V)
[PROOF STEP]
unfolding morphism_sheaves_of_rings_def
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings Y is_open\<^sub>Y \<O>\<^sub>Y \<rho>\<^sub>Y d add_str\<^sub>Y mult_str\<^sub>Y zero_str\<^sub>Y one_str\<^sub>Y local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<phi>\<^sub>f
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (?fam_morphisms ?U) (?\<FF> ?U) (?\<FF>' ?U)

goal (1 subgoal):
 1. \<phi>\<^sub>f V q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X V)
[PROOF STEP]
by (metis assms local.im_sheaf_def map.map_closed)