[STATEMENT]
lemma sheaf_spec_morphisms_are_ring_morphisms:
  assumes U: "is_zariski_open U" and V: "is_zariski_open V" and "V \<subseteq> U"
  shows "ring_homomorphism (sheaf_spec_morphisms U V)
                           (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
                           (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
 2. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 3. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 4. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
 5. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
 6. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 7. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 8. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 9. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 10. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
A total of 13 subgoals...
[PROOF STEP]
show "Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
by (simp add: assms sheaf_spec_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)

goal (12 subgoals):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 2. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 3. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
 4. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
 5. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 6. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 7. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 8. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 9. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 10. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
A total of 12 subgoals...
[PROOF STEP]
show "Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF U]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)

goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)

goal (11 subgoals):
 1. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 2. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
 3. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
 4. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 5. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 6. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 7. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 8. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 9. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 10. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
A total of 11 subgoals...
[PROOF STEP]
show "Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF U]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)

goal (1 subgoal):
 1. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)

goal (10 subgoals):
 1. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
 2. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
 3. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 4. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 5. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 6. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 7. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 8. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 9. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 10. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF U]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)

goal (1 subgoal):
 1. commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
[PROOF STATE]
proof (state)
this:
commutative_monoid_axioms (\<O> U) (add_sheaf_spec U)

goal (9 subgoals):
 1. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
 2. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 3. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 4. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 5. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 6. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 7. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 8. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 9. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)
[PROOF STEP]
by (meson U comm_ring_def ring_def sheaf_spec_on_open_is_comm_ring)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)

goal (8 subgoals):
 1. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
 2. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 3. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 4. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 5. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 6. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 7. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 8. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
[PROOF STEP]
by (meson U comm_ring.axioms(1) ring_def sheaf_spec_on_open_is_comm_ring)
[PROOF STATE]
proof (state)
this:
ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)

goal (7 subgoals):
 1. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 2. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 3. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 4. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 5. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 6. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 7. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF V]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)

goal (1 subgoal):
 1. Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)

goal (6 subgoals):
 1. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
 2. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 3. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 4. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 5. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 6. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF V]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)

goal (1 subgoal):
 1. Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (\<O> V) (add_sheaf_spec V) (zero_sheaf_spec V)

goal (5 subgoals):
 1. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
 2. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 3. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 4. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 5. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
[PROOF STEP]
using sheaf_spec_on_open_is_comm_ring [OF V]
[PROOF STATE]
proof (prove)
using this:
comm_ring (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)

goal (1 subgoal):
 1. commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)
[PROOF STEP]
by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
[PROOF STATE]
proof (state)
this:
commutative_monoid_axioms (\<O> V) (add_sheaf_spec V)

goal (4 subgoals):
 1. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
 2. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 3. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 4. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
by (meson V comm_ring.axioms(1) ring_def sheaf_spec_on_open_is_comm_ring)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> V) (mult_sheaf_spec V) (one_sheaf_spec V)

goal (3 subgoals):
 1. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
 2. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 3. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)
[PROOF STEP]
by (meson V comm_ring_def ring_def sheaf_spec_on_open_is_comm_ring)
[PROOF STATE]
proof (state)
this:
ring_axioms (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V)

goal (2 subgoals):
 1. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
 2. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U)
              (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
assume xy: "x \<in> \<O> U" "y \<in> \<O> U"
[PROOF STATE]
proof (state)
this:
x \<in> \<O> U
y \<in> \<O> U

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
have "sheaf_spec_morphisms U V (add_sheaf_spec U x y) = restrict (add_sheaf_spec U x y) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (add_sheaf_spec U x y) = restrict (add_sheaf_spec U x y) V
[PROOF STEP]
by (simp add: U add_sheaf_spec_in_sheaf_spec comm_ring.zariski_open_is_subset local.comm_ring_axioms sheaf_spec_morphisms_def xy)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (add_sheaf_spec U x y) = restrict (add_sheaf_spec U x y) V

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (add_sheaf_spec U x y) = restrict (add_sheaf_spec U x y) V

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
have "... = add_sheaf_spec V (restrict x V) (restrict y V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (add_sheaf_spec U x y) V = add_sheaf_spec V (restrict x V) (restrict y V)
[PROOF STEP]
using add_sheaf_spec_def \<open>V \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
add_sheaf_spec ?U ?s ?s' \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (?s \<pp>) (?s' \<pp>)
V \<subseteq> U

goal (1 subgoal):
 1. restrict (add_sheaf_spec U x y) V = add_sheaf_spec V (restrict x V) (restrict y V)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
restrict (add_sheaf_spec U x y) V = add_sheaf_spec V (restrict x V) (restrict y V)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
restrict (add_sheaf_spec U x y) V = add_sheaf_spec V (restrict x V) (restrict y V)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
have "... = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec V (restrict x V) (restrict y V) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
by (simp add: sheaf_spec_morphisms_def xy)
[PROOF STATE]
proof (state)
this:
add_sheaf_spec V (restrict x V) (restrict y V) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
show "sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
have "sheaf_spec_morphisms U V (zero_sheaf_spec U) = restrict (zero_sheaf_spec U) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = restrict (zero_sheaf_spec U) V
[PROOF STEP]
by (simp add: U comm_ring.sheaf_spec_morphisms_def local.comm_ring_axioms zero_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (zero_sheaf_spec U) = restrict (zero_sheaf_spec U) V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (zero_sheaf_spec U) = restrict (zero_sheaf_spec U) V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
have "... = zero_sheaf_spec V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (zero_sheaf_spec U) V = zero_sheaf_spec V
[PROOF STEP]
by (metis FuncSet.restrict_restrict assms(3) inf.absorb_iff2 zero_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
restrict (zero_sheaf_spec U) V = zero_sheaf_spec V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
show "sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V

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

goal (1 subgoal):
 1. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
show "monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U)
              (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
assume xy: "x \<in> \<O> U" "y \<in> \<O> U"
[PROOF STATE]
proof (state)
this:
x \<in> \<O> U
y \<in> \<O> U

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
have "sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = restrict (mult_sheaf_spec U x y) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = restrict (mult_sheaf_spec U x y) V
[PROOF STEP]
by (simp add: U mult_sheaf_spec_in_sheaf_spec comm_ring.zariski_open_is_subset local.comm_ring_axioms sheaf_spec_morphisms_def xy)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = restrict (mult_sheaf_spec U x y) V

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = restrict (mult_sheaf_spec U x y) V

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
have "... = mult_sheaf_spec V (restrict x V) (restrict y V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (mult_sheaf_spec U x y) V = mult_sheaf_spec V (restrict x V) (restrict y V)
[PROOF STEP]
using mult_sheaf_spec_def \<open>V \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
mult_sheaf_spec ?U ?s ?s' \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (?s \<pp>) (?s' \<pp>)
V \<subseteq> U

goal (1 subgoal):
 1. restrict (mult_sheaf_spec U x y) V = mult_sheaf_spec V (restrict x V) (restrict y V)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
restrict (mult_sheaf_spec U x y) V = mult_sheaf_spec V (restrict x V) (restrict y V)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
restrict (mult_sheaf_spec U x y) V = mult_sheaf_spec V (restrict x V) (restrict y V)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
have "... = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec V (restrict x V) (restrict y V) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
by (simp add: sheaf_spec_morphisms_def xy)
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec V (restrict x V) (restrict y V) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
 2. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
show "sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
have "sheaf_spec_morphisms U V (one_sheaf_spec U) = restrict (one_sheaf_spec U) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = restrict (one_sheaf_spec U) V
[PROOF STEP]
by (simp add: U comm_ring.sheaf_spec_morphisms_def local.comm_ring_axioms one_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (one_sheaf_spec U) = restrict (one_sheaf_spec U) V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (one_sheaf_spec U) = restrict (one_sheaf_spec U) V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
have "... = one_sheaf_spec V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (one_sheaf_spec U) V = one_sheaf_spec V
[PROOF STEP]
by (metis FuncSet.restrict_restrict assms(3) inf.absorb_iff2 one_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
restrict (one_sheaf_spec U) V = one_sheaf_spec V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
show "sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V

goal (1 subgoal):
 1. sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sheaf_spec_is_presheaf:
  shows "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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
have "sheaf_spec {} = {\<O>b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<O> {} = {\<O>b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<O> {} \<subseteq> {\<O>b}
 2. {\<O>b} \<subseteq> \<O> {}
[PROOF STEP]
show "{\<O>b} \<subseteq> \<O> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<O>b} \<subseteq> \<O> {}
[PROOF STEP]
using undefined_is_map_on_empty map_on_empty_is_regular sheaf_spec_def \<O>_on_emptyset
[PROOF STATE]
proof (prove)
using this:
?f = (\<lambda>x. undefined) \<Longrightarrow> Set_Theory.map ?f {} {}
is_regular ?s {}
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}
\<O> {} = {\<O>b}

goal (1 subgoal):
 1. {\<O>b} \<subseteq> \<O> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{\<O>b} \<subseteq> \<O> {}

goal (1 subgoal):
 1. \<O> {} \<subseteq> {\<O>b}
[PROOF STEP]
thus "\<O> {} \<subseteq> {\<O>b}"
[PROOF STATE]
proof (prove)
using this:
{\<O>b} \<subseteq> \<O> {}

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

goal (1 subgoal):
 1. \<O> {} \<subseteq> {\<O>b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<O> {} \<subseteq> {\<O>b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<O> {} = {\<O>b}

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<O> {} = {\<O>b}

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
have "\<And>U. is_zariski_open U \<Longrightarrow> (\<And>s. s \<in> (\<O> U) \<Longrightarrow> sheaf_spec_morphisms U U s = s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_zariski_open U \<Longrightarrow> (\<And>s. s \<in> \<O> U \<Longrightarrow> sheaf_spec_morphisms U U s = s)
[PROOF STEP]
using sheaf_spec_morphisms_def sheaf_morphisms_sheaf_spec
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V
?s \<in> \<O> ?U \<Longrightarrow> sheaf_spec_morphisms ?U ?U ?s = ?s

goal (1 subgoal):
 1. \<And>U. is_zariski_open U \<Longrightarrow> (\<And>s. s \<in> \<O> U \<Longrightarrow> sheaf_spec_morphisms U U s = s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
have "sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s"
    if "is_zariski_open U" "is_zariski_open V" "is_zariski_open W" "V \<subseteq> U" "W \<subseteq> V" and "s \<in> \<O> U"
    for U V W s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s
[PROOF STEP]
have "restrict s V \<in> \<O> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict s V \<in> \<O> V
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
is_zariski_open V
is_zariski_open W
V \<subseteq> U
W \<subseteq> V
s \<in> \<O> U

goal (1 subgoal):
 1. restrict s V \<in> \<O> V
[PROOF STEP]
by (smt map.map_closed restrict_apply sheaf_spec_morphisms_are_maps sheaf_spec_morphisms_def)
[PROOF STATE]
proof (state)
this:
restrict s V \<in> \<O> V

goal (1 subgoal):
 1. sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
is_zariski_open U
is_zariski_open V
is_zariski_open W
V \<subseteq> U
W \<subseteq> V
s \<in> \<O> U
restrict s V \<in> \<O> V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
is_zariski_open V
is_zariski_open W
V \<subseteq> U
W \<subseteq> V
s \<in> \<O> U
restrict s V \<in> \<O> V

goal (1 subgoal):
 1. sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s
[PROOF STEP]
by (simp add: sheaf_spec_morphisms_def inf_absorb2)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_zariski_open ?U3; is_zariski_open ?V3; is_zariski_open ?W3; ?V3 \<subseteq> ?U3; ?W3 \<subseteq> ?V3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?W3 ?s3 = (sheaf_spec_morphisms ?V3 ?W3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?s3

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<O> {} = {\<O>b}
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3
\<lbrakk>is_zariski_open ?U3; is_zariski_open ?V3; is_zariski_open ?W3; ?V3 \<subseteq> ?U3; ?W3 \<subseteq> ?V3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?W3 ?s3 = (sheaf_spec_morphisms ?V3 ?W3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?s3
[PROOF STEP]
show "presheaf_of_rings_axioms 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)
using this:
\<O> {} = {\<O>b}
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3
\<lbrakk>is_zariski_open ?U3; is_zariski_open ?V3; is_zariski_open ?W3; ?V3 \<subseteq> ?U3; ?W3 \<subseteq> ?V3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?W3 ?s3 = (sheaf_spec_morphisms ?V3 ?W3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?s3

goal (1 subgoal):
 1. presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
unfolding presheaf_of_rings_def presheaf_of_rings_axioms_def
[PROOF STATE]
proof (prove)
using this:
\<O> {} = {\<O>b}
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3
\<lbrakk>is_zariski_open ?U3; is_zariski_open ?V3; is_zariski_open ?W3; ?V3 \<subseteq> ?U3; ?W3 \<subseteq> ?V3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?W3 ?s3 = (sheaf_spec_morphisms ?V3 ?W3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?s3

goal (1 subgoal):
 1. ((\<forall>U V. is_zariski_open U \<longrightarrow> is_zariski_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> ring_homomorphism (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)) \<and> \<O> {} = {\<O>b}) \<and> (\<forall>U. is_zariski_open U \<longrightarrow> (\<forall>x. x \<in> \<O> U \<longrightarrow> sheaf_spec_morphisms U U x = x)) \<and> (\<forall>U V W. is_zariski_open U \<longrightarrow> is_zariski_open V \<longrightarrow> is_zariski_open W \<longrightarrow> V \<subseteq> U \<longrightarrow> W \<subseteq> V \<longrightarrow> (\<forall>x. x \<in> \<O> U \<longrightarrow> sheaf_spec_morphisms U W x = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) x))
[PROOF STEP]
using sheaf_spec_morphisms_are_ring_morphisms
[PROOF STATE]
proof (prove)
using this:
\<O> {} = {\<O>b}
\<lbrakk>is_zariski_open ?U3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?U3 ?s3 = ?s3
\<lbrakk>is_zariski_open ?U3; is_zariski_open ?V3; is_zariski_open ?W3; ?V3 \<subseteq> ?U3; ?W3 \<subseteq> ?V3; ?s3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms ?U3 ?W3 ?s3 = (sheaf_spec_morphisms ?V3 ?W3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?s3
\<lbrakk>is_zariski_open ?U; is_zariski_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (sheaf_spec_morphisms ?U ?V) (\<O> ?U) (add_sheaf_spec ?U) (mult_sheaf_spec ?U) (zero_sheaf_spec ?U) (one_sheaf_spec ?U) (\<O> ?V) (add_sheaf_spec ?V) (mult_sheaf_spec ?V) (zero_sheaf_spec ?V) (one_sheaf_spec ?V)

goal (1 subgoal):
 1. ((\<forall>U V. is_zariski_open U \<longrightarrow> is_zariski_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> ring_homomorphism (sheaf_spec_morphisms U V) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) (\<O> V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)) \<and> \<O> {} = {\<O>b}) \<and> (\<forall>U. is_zariski_open U \<longrightarrow> (\<forall>x. x \<in> \<O> U \<longrightarrow> sheaf_spec_morphisms U U x = x)) \<and> (\<forall>U V W. is_zariski_open U \<longrightarrow> is_zariski_open V \<longrightarrow> is_zariski_open W \<longrightarrow> V \<subseteq> U \<longrightarrow> W \<subseteq> V \<longrightarrow> (\<forall>x. x \<in> \<O> U \<longrightarrow> sheaf_spec_morphisms U W x = (sheaf_spec_morphisms V W \<circ> sheaf_spec_morphisms U V) x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
presheaf_of_rings_axioms is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sheaf_spec_is_sheaf:
  shows "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]
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 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
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 3. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
show "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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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
[PROOF STEP]
using sheaf_spec_is_presheaf
[PROOF STATE]
proof (prove)
using this:
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

goal (1 subgoal):
 1. 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
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
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

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
fix U I V s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
assume H: "open_cover_of_open_subset Spec is_zariski_open U I V"
                        "\<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U"
                        "s \<in> \<O> U"
                        "\<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset Spec is_zariski_open U I V
?i3 \<in> I \<Longrightarrow> V ?i3 \<subseteq> U
s \<in> \<O> U
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) s = zero_sheaf_spec (V ?i3)

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open_cover_of_open_subset Spec is_zariski_open U I V
?i3 \<in> I \<Longrightarrow> V ?i3 \<subseteq> U
s \<in> \<O> U
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) s = zero_sheaf_spec (V ?i3)
[PROOF STEP]
have "s \<pp> = zero_sheaf_spec U \<pp>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset Spec is_zariski_open U I V
?i3 \<in> I \<Longrightarrow> V ?i3 \<subseteq> U
s \<in> \<O> U
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) s = zero_sheaf_spec (V ?i3)

goal (1 subgoal):
 1. s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
\<pp> \<in> U
[PROOF STEP]
obtain i where F: "i \<in> I" "\<pp> \<in> (V i)" "is_zariski_open (V i)"
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> I; \<pp> \<in> V i; is_zariski_open (V i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
open_cover_of_open_subset Spec is_zariski_open U I V

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> I; \<pp> \<in> V i; is_zariski_open (V i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding open_cover_of_subset_def open_cover_of_open_subset_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
(topological_space Spec is_zariski_open \<and> cover_of_subset Spec U I V \<and> open_cover_of_subset_axioms is_zariski_open I V) \<and> open_cover_of_open_subset_axioms is_zariski_open U

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> I; \<pp> \<in> V i; is_zariski_open (V i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs open_cover_of_subset_axioms_def)
[PROOF STATE]
proof (state)
this:
i \<in> I
\<pp> \<in> V i
is_zariski_open (V i)

goal (1 subgoal):
 1. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> I
\<pp> \<in> V i
is_zariski_open (V i)
[PROOF STEP]
have "sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R \<setminus> \<pp>) R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
using this:
i \<in> I
\<pp> \<in> V i
is_zariski_open (V i)

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using H(2,4) F
[PROOF STATE]
proof (prove)
using this:
i \<in> I
\<pp> \<in> V i
is_zariski_open (V i)
?i3 \<in> I \<Longrightarrow> V ?i3 \<subseteq> U
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) s = zero_sheaf_spec (V ?i3)
i \<in> I
\<pp> \<in> V i
is_zariski_open (V i)

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (simp add: zero_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
thus "s \<pp> = zero_sheaf_spec U \<pp>"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
using sheaf_spec_morphisms_def zero_sheaf_spec_def F(2)
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U (V i) s \<pp> = quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V
zero_sheaf_spec ?U \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
\<pp> \<in> V i

goal (1 subgoal):
 1. s \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
by (simp add: H(3) \<open>\<pp> \<in> U\<close>)
[PROOF STATE]
proof (state)
this:
s \<pp> = zero_sheaf_spec U \<pp>

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

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> s ?\<pp>3 = zero_sheaf_spec U ?\<pp>3

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
have "s \<in> extensional U" " zero_sheaf_spec U \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> extensional U &&& zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
by (simp_all add: H(3))
[PROOF STATE]
proof (state)
this:
s \<in> extensional U
zero_sheaf_spec U \<in> extensional U

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> \<O> U; \<And>i. i \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)\<rbrakk> \<Longrightarrow> s = zero_sheaf_spec U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> s ?\<pp>3 = zero_sheaf_spec U ?\<pp>3
s \<in> extensional U
zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
show "s = zero_sheaf_spec U"
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> s ?\<pp>3 = zero_sheaf_spec U ?\<pp>3
s \<in> extensional U
zero_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. s = zero_sheaf_spec U
[PROOF STEP]
using extensionalityI
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> s ?\<pp>3 = zero_sheaf_spec U ?\<pp>3
s \<in> extensional U
zero_sheaf_spec U \<in> extensional U
\<lbrakk>?f \<in> extensional ?A; ?g \<in> extensional ?A; \<And>x. x \<in> ?A \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. s = zero_sheaf_spec U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = zero_sheaf_spec U

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
fix U I V s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
assume H: "open_cover_of_open_subset Spec is_zariski_open U I V"
                        "\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> (V i)"
                        "\<And>i j. i \<in> I \<Longrightarrow>
                                  j \<in> I \<Longrightarrow>
                                    sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) =
                                    sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset Spec is_zariski_open U I V
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i
\<lbrakk>?i3 \<in> I; ?j3 \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V ?i3) (V ?i3 \<inter> V ?j3) (s ?i3) = sheaf_spec_morphisms (V ?j3) (V ?i3 \<inter> V ?j3) (s ?j3)

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
define t where D: "t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>"
[PROOF STATE]
proof (state)
this:
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>
[PROOF STEP]
have F1: "s i \<pp> = s j \<pp>" if "i \<in> I" "j \<in> I" "\<pp> \<in> V i" "\<pp> \<in> V j" for \<pp> i j
[PROOF STATE]
proof (prove)
using this:
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>

goal (1 subgoal):
 1. s i \<pp> = s j \<pp>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
have "s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>
[PROOF STEP]
using that sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
using this:
i \<in> I
j \<in> I
\<pp> \<in> V i
\<pp> \<in> V j
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V

goal (1 subgoal):
 1. s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>
[PROOF STEP]
by (simp add: H(2))
[PROOF STATE]
proof (state)
this:
s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>

goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>

goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
have "\<dots> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>
[PROOF STEP]
using H(3) that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i3 \<in> I; ?j3 \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V ?i3) (V ?i3 \<inter> V ?j3) (s ?i3) = sheaf_spec_morphisms (V ?j3) (V ?i3 \<inter> V ?j3) (s ?j3)
i \<in> I
j \<in> I
\<pp> \<in> V i
\<pp> \<in> V j

goal (1 subgoal):
 1. sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>

goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>

goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
have "\<dots> = s j \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp> = s j \<pp>
[PROOF STEP]
using sheaf_spec_morphisms_def that
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V
i \<in> I
j \<in> I
\<pp> \<in> V i
\<pp> \<in> V j

goal (1 subgoal):
 1. sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp> = s j \<pp>
[PROOF STEP]
by (simp add: H(2))
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp> = s j \<pp>

goal (1 subgoal):
 1. t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp> \<Longrightarrow> s i \<pp> = s j \<pp>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>
sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>
sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp> = s j \<pp>
[PROOF STEP]
show "s i \<pp> = s j \<pp>"
[PROOF STATE]
proof (prove)
using this:
s i \<pp> = sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp>
sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) \<pp> = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp>
sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j) \<pp> = s j \<pp>

goal (1 subgoal):
 1. s i \<pp> = s j \<pp>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s i \<pp> = s j \<pp>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i3 \<in> I; ?j3 \<in> I; ?\<pp>3 \<in> V ?i3; ?\<pp>3 \<in> V ?j3\<rbrakk> \<Longrightarrow> s ?i3 ?\<pp>3 = s ?j3 ?\<pp>3

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
have "t \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<O> U
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> \<O> U
[PROOF STEP]
have "t \<pp> \<in> (R\<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)" if "\<pp>\<in>U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
using D H(1) H(2) cover_of_subset.cover_of_select_index
        cover_of_subset.select_index_belongs open_cover_of_open_subset.axioms(1)
        open_cover_of_subset_def sec_has_right_codom that
[PROOF STATE]
proof (prove)
using this:
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>
open_cover_of_open_subset Spec is_zariski_open U I V
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i
\<lbrakk>cover_of_subset ?X ?U ?index ?cover; ?x \<in> ?U\<rbrakk> \<Longrightarrow> ?x \<in> ?cover (cover_of_subset.select_index ?index ?cover ?x)
\<lbrakk>cover_of_subset ?X ?U ?index ?cover; ?x \<in> ?U\<rbrakk> \<Longrightarrow> cover_of_subset.select_index ?index ?cover ?x \<in> ?index
open_cover_of_open_subset ?X ?is_open ?U ?I ?C \<Longrightarrow> open_cover_of_subset ?X ?is_open ?U ?I ?C
open_cover_of_subset ?X ?is_open ?U ?I ?C \<equiv> topological_space ?X ?is_open \<and> cover_of_subset ?X ?U ?I ?C \<and> open_cover_of_subset_axioms ?is_open ?I ?C
\<lbrakk>?s \<in> \<O> ?U; ?\<pp> \<in> ?U\<rbrakk> \<Longrightarrow> ?s ?\<pp> \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>
\<pp> \<in> U

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

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

goal (1 subgoal):
 1. t \<in> \<O> U
[PROOF STEP]
have "t \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> extensional U
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>

goal (1 subgoal):
 1. t \<in> extensional U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> extensional U

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

goal (1 subgoal):
 1. t \<in> \<O> U
[PROOF STEP]
have "is_regular t U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular t U
[PROOF STEP]
unfolding is_regular_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V)
[PROOF STEP]
proof (intro strip conjI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pp>. \<pp> \<in> U \<Longrightarrow> \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pp>. \<pp> \<in> U \<Longrightarrow> \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (1 subgoal):
 1. \<And>\<pp>. \<pp> \<in> U \<Longrightarrow> \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
show "\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
have cov_in_I: "cover_of_subset.select_index I V \<pp> \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cover_of_subset.select_index I V \<pp> \<in> I
[PROOF STEP]
by (meson H(1) \<open>\<pp> \<in> U\<close> cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
[PROOF STATE]
proof (state)
this:
cover_of_subset.select_index I V \<pp> \<in> I

goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
have V: "V (cover_of_subset.select_index I V \<pp>) \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V (cover_of_subset.select_index I V \<pp>) \<subseteq> U
[PROOF STEP]
using H(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i

goal (1 subgoal):
 1. V (cover_of_subset.select_index I V \<pp>) \<subseteq> U
[PROOF STEP]
by (meson H(1) \<open>\<pp> \<in> U\<close> cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
[PROOF STATE]
proof (state)
this:
V (cover_of_subset.select_index I V \<pp>) \<subseteq> U

goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
have V2: "\<exists>V'. is_zariski_open V' \<and> V'\<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and>
                 is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'
[PROOF STEP]
using H(1,2)
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset Spec is_zariski_open U I V
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i

goal (1 subgoal):
 1. \<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'
[PROOF STEP]
unfolding sheaf_spec_def open_cover_of_open_subset_def open_cover_of_subset_def is_regular_def
[PROOF STATE]
proof (prove)
using this:
(topological_space Spec is_zariski_open \<and> cover_of_subset Spec U I V \<and> open_cover_of_subset_axioms is_zariski_open I V) \<and> open_cover_of_open_subset_axioms is_zariski_open U
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>V i. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. \<forall>\<pp>. \<pp> \<in> V i \<longrightarrow> (\<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V i \<and> \<pp> \<in> Va \<and> is_locally_frac s Va)}

goal (1 subgoal):
 1. \<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> cov_in_I cover_of_subset.cover_of_select_index
[PROOF STATE]
proof (prove)
using this:
(topological_space Spec is_zariski_open \<and> cover_of_subset Spec U I V \<and> open_cover_of_subset_axioms is_zariski_open I V) \<and> open_cover_of_open_subset_axioms is_zariski_open U
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>V i. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. \<forall>\<pp>. \<pp> \<in> V i \<longrightarrow> (\<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V i \<and> \<pp> \<in> Va \<and> is_locally_frac s Va)}
\<pp> \<in> U
cover_of_subset.select_index I V \<pp> \<in> I
\<lbrakk>cover_of_subset ?X ?U ?index ?cover; ?x \<in> ?U\<rbrakk> \<Longrightarrow> ?x \<in> ?cover (cover_of_subset.select_index ?index ?cover ?x)

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

goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
have "\<And>V' \<qq>. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<Longrightarrow> \<qq> \<in> V' \<Longrightarrow> t \<qq> = s (cover_of_subset.select_index I V \<pp>) \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V' \<qq>. \<lbrakk>is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>); \<qq> \<in> V'\<rbrakk> \<Longrightarrow> t \<qq> = s (cover_of_subset.select_index I V \<pp>) \<qq>
[PROOF STEP]
by (smt D F1 H(1) V \<open>\<pp> \<in> U\<close> cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def restrict_apply subsetD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_zariski_open ?V'3 \<and> ?V'3 \<subseteq> V (cover_of_subset.select_index I V \<pp>); ?\<qq>3 \<in> ?V'3\<rbrakk> \<Longrightarrow> t ?\<qq>3 = s (cover_of_subset.select_index I V \<pp>) ?\<qq>3

goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
with V V2
[PROOF STATE]
proof (chain)
picking this:
V (cover_of_subset.select_index I V \<pp>) \<subseteq> U
\<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'
\<lbrakk>is_zariski_open ?V'3 \<and> ?V'3 \<subseteq> V (cover_of_subset.select_index I V \<pp>); ?\<qq>3 \<in> ?V'3\<rbrakk> \<Longrightarrow> t ?\<qq>3 = s (cover_of_subset.select_index I V \<pp>) ?\<qq>3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V (cover_of_subset.select_index I V \<pp>) \<subseteq> U
\<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> is_locally_frac (s (cover_of_subset.select_index I V \<pp>)) V'
\<lbrakk>is_zariski_open ?V'3 \<and> ?V'3 \<subseteq> V (cover_of_subset.select_index I V \<pp>); ?\<qq>3 \<in> ?V'3\<rbrakk> \<Longrightarrow> t ?\<qq>3 = s (cover_of_subset.select_index I V \<pp>) ?\<qq>3

goal (1 subgoal):
 1. \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac t V
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V (cover_of_subset.select_index I V \<pp>) \<subseteq> U
\<exists>V'. is_zariski_open V' \<and> V' \<subseteq> V (cover_of_subset.select_index I V \<pp>) \<and> \<pp> \<in> V' \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V'. f \<notin> \<qq> \<and> s (cover_of_subset.select_index I V \<pp>) \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))
\<lbrakk>is_zariski_open ?V'3 \<and> ?V'3 \<subseteq> V (cover_of_subset.select_index I V \<pp>); ?\<qq>3 \<in> ?V'3\<rbrakk> \<Longrightarrow> t ?\<qq>3 = s (cover_of_subset.select_index I V \<pp>) ?\<qq>3

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
have "sheaf_spec_morphisms U (V i) t = s i" if "i \<in> I" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t = s i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. sheaf_spec_morphisms U (V i) t x = s i x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. sheaf_spec_morphisms U (V i) t x = s i x
[PROOF STEP]
have "sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>" if "\<pp> \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
from that H(1)
[PROOF STATE]
proof (chain)
picking this:
\<pp> \<in> U
open_cover_of_open_subset Spec is_zariski_open U I V
[PROOF STEP]
obtain j where "j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp>"
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
open_cover_of_open_subset Spec is_zariski_open U I V

goal (1 subgoal):
 1. (\<And>j. j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding D open_cover_of_subset_def open_cover_of_open_subset_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
(topological_space Spec is_zariski_open \<and> cover_of_subset Spec U I V \<and> open_cover_of_subset_axioms is_zariski_open I V) \<and> open_cover_of_open_subset_axioms is_zariski_open U

goal (1 subgoal):
 1. (\<And>j. j \<in> I \<and> \<pp> \<in> V j \<and> (\<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>) \<pp> = s j \<pp> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs restrict_apply')
[PROOF STATE]
proof (state)
this:
j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp>

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
thus "sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>"
[PROOF STATE]
proof (prove)
using this:
j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp>

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
using \<open>t \<in> \<O> U\<close> \<open>i \<in> I\<close> H(2) that
[PROOF STATE]
proof (prove)
using this:
j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp>
t \<in> \<O> U
i \<in> I
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i
\<pp> \<in> U

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
unfolding sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
using this:
j \<in> I \<and> \<pp> \<in> V j \<and> t \<pp> = s j \<pp>
t \<in> \<O> U
i \<in> I
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>s\<in>\<O> U. restrict s (V i)) t \<pp> = s i \<pp>
[PROOF STEP]
apply (simp add: D split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<in> I \<and> \<pp> \<in> V j \<and> s (cover_of_subset.select_index I V \<pp>) \<pp> = s j \<pp>; (\<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>) \<in> \<O> U; i \<in> I; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<pp> \<in> U\<rbrakk> \<Longrightarrow> (\<pp> \<in> V i \<longrightarrow> s j \<pp> = s i \<pp>) \<and> (\<pp> \<notin> V i \<longrightarrow> undefined = s i \<pp>)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) F1  extensional_arb [OF sec_is_extensional])
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U \<Longrightarrow> sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>

goal (1 subgoal):
 1. \<And>x. sheaf_spec_morphisms U (V i) t x = s i x
[PROOF STEP]
thus "sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>"
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U \<Longrightarrow> sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
using sheaf_spec_morphisms_def D F1
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U \<Longrightarrow> sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V
t \<equiv> \<lambda>\<pp>\<in>U. s (cover_of_subset.select_index I V \<pp>) \<pp>
\<lbrakk>?i3 \<in> I; ?j3 \<in> I; ?\<pp>3 \<in> V ?i3; ?\<pp>3 \<in> V ?j3\<rbrakk> \<Longrightarrow> s ?i3 ?\<pp>3 = s ?j3 ?\<pp>3

goal (1 subgoal):
 1. sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>
[PROOF STEP]
by (smt H(2) \<open>i \<in> I\<close> \<open>t \<in> \<O> U\<close> comm_ring.sheaf_morphisms_sheaf_spec local.comm_ring_axioms restrict_apply subsetD)
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (V i) t \<pp> = s i \<pp>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) t = s ?i3

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset Spec is_zariski_open U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> \<O> V i; \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> sheaf_spec_morphisms (V i) (V i \<inter> V j) (s i) = sheaf_spec_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
thus "\<exists>t. t \<in> (\<O> U) \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)"
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) t = s ?i3

goal (1 subgoal):
 1. \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
using \<open>t \<in> \<O> U\<close>
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> I \<Longrightarrow> sheaf_spec_morphisms U (V ?i3) t = s ?i3
t \<in> \<O> U

goal (1 subgoal):
 1. \<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. t \<in> \<O> U \<and> (\<forall>i. i \<in> I \<longrightarrow> sheaf_spec_morphisms U (V i) t = s i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shrinking:
  assumes "is_zariski_open U" and "\<pp> \<in> U" and "s \<in> \<O> U" and "t \<in> \<O> U"
  obtains V a f b g where "is_zariski_open V" "V \<subseteq> U" "\<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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> U; \<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) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> U; \<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) \<Longrightarrow> thesis
[PROOF STEP]
obtain Vs a f where "is_zariski_open Vs" "Vs \<subseteq> U" "\<pp> \<in> Vs" "a \<in> R" "f \<in> R"
"\<And>\<qq>. \<qq> \<in> Vs \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs a f. \<lbrakk>is_zariski_open Vs; Vs \<subseteq> U; \<pp> \<in> Vs; a \<in> R; f \<in> R; \<And>\<qq>. \<qq> \<in> Vs \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2,3) sheaf_spec_def is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
s \<in> \<O> U
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}
is_regular ?s ?U \<equiv> \<forall>\<pp>. \<pp> \<in> ?U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> ?U \<and> \<pp> \<in> V \<and> is_locally_frac ?s V)
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. (\<And>Vs a f. \<lbrakk>is_zariski_open Vs; Vs \<subseteq> U; \<pp> \<in> Vs; a \<in> R; f \<in> R; \<And>\<qq>. \<qq> \<in> Vs \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_zariski_open Vs
Vs \<subseteq> U
\<pp> \<in> Vs
a \<in> R
f \<in> R
?\<qq>3 \<in> Vs \<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. (\<And>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> U; \<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) \<Longrightarrow> thesis
[PROOF STEP]
obtain Vt b g where "is_zariski_open Vt" "Vt \<subseteq> U" "\<pp> \<in> Vt" "b \<in> R" "g \<in> R"
"\<And>\<qq>. \<qq> \<in> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vt b g. \<lbrakk>is_zariski_open Vt; Vt \<subseteq> U; \<pp> \<in> Vt; b \<in> R; g \<in> R; \<And>\<qq>. \<qq> \<in> Vt \<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 assms(2,4) sheaf_spec_def is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
t \<in> \<O> U
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}
is_regular ?s ?U \<equiv> \<forall>\<pp>. \<pp> \<in> ?U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> ?U \<and> \<pp> \<in> V \<and> is_locally_frac ?s V)
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. (\<And>Vt b g. \<lbrakk>is_zariski_open Vt; Vt \<subseteq> U; \<pp> \<in> Vt; b \<in> R; g \<in> R; \<And>\<qq>. \<qq> \<in> Vt \<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 auto
[PROOF STATE]
proof (state)
this:
is_zariski_open Vt
Vt \<subseteq> U
\<pp> \<in> Vt
b \<in> R
g \<in> R
?\<qq>3 \<in> Vt \<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>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> U; \<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) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_zariski_open Vt
Vt \<subseteq> U
\<pp> \<in> Vt
b \<in> R
g \<in> R
?\<qq>3 \<in> Vt \<Longrightarrow> g \<notin> ?\<qq>3 \<and> t ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
have "is_zariski_open (Vs \<inter> Vt)" "Vs \<inter> Vt \<subseteq> U" "\<pp> \<in> Vs \<inter> Vt"
"\<And>\<qq>. \<qq> \<in> (Vs \<inter> Vt) \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f"
"\<And>\<qq>. \<qq> \<in> (Vs \<inter> Vt) \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g"
[PROOF STATE]
proof (prove)
using this:
is_zariski_open Vt
Vt \<subseteq> U
\<pp> \<in> Vt
b \<in> R
g \<in> R
?\<qq>3 \<in> Vt \<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. (is_zariski_open (Vs \<inter> Vt) &&& Vs \<inter> Vt \<subseteq> U) &&& \<pp> \<in> Vs \<inter> Vt &&& (\<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f) &&& (\<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
[PROOF STEP]
using topological_space.open_inter
[PROOF STATE]
proof (prove)
using this:
is_zariski_open Vt
Vt \<subseteq> U
\<pp> \<in> Vt
b \<in> R
g \<in> R
?\<qq>3 \<in> Vt \<Longrightarrow> g \<notin> ?\<qq>3 \<and> t ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> b g
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U; ?is_open ?V\<rbrakk> \<Longrightarrow> ?is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. (is_zariski_open (Vs \<inter> Vt) &&& Vs \<inter> Vt \<subseteq> U) &&& \<pp> \<in> Vs \<inter> Vt &&& (\<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f) &&& (\<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g)
[PROOF STEP]
apply (simp add: \<open>is_zariski_open Vs\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Vs \<inter> Vt \<subseteq> U
 2. \<pp> \<in> Vs \<inter> Vt
 3. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f
 4. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
using \<open>Vs \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
Vs \<subseteq> U

goal (4 subgoals):
 1. Vs \<inter> Vt \<subseteq> U
 2. \<pp> \<in> Vs \<inter> Vt
 3. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f
 4. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pp> \<in> Vs \<inter> Vt
 2. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f
 3. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
apply (simp add: \<open>\<pp> \<in> Vs\<close> \<open>\<pp> \<in> Vt\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f
 2. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
apply (simp add: \<open>\<And>\<qq>. \<qq> \<in> Vs \<Longrightarrow> f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> a f\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<qq>. \<qq> \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g
[PROOF STEP]
by (simp add: \<open>\<And>\<qq>. \<qq> \<in> Vt \<Longrightarrow> g \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> b g\<close>)
[PROOF STATE]
proof (state)
this:
is_zariski_open (Vs \<inter> Vt)
Vs \<inter> Vt \<subseteq> U
\<pp> \<in> Vs \<inter> Vt
?\<qq>3 \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> ?\<qq>3 \<and> s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> a f
?\<qq>3 \<in> Vs \<inter> Vt \<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>V a f b g. \<lbrakk>is_zariski_open V; V \<subseteq> U; \<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) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zariski_open (Vs \<inter> Vt)
Vs \<inter> Vt \<subseteq> U
\<pp> \<in> Vs \<inter> Vt
?\<qq>3 \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> ?\<qq>3 \<and> s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> a f
?\<qq>3 \<in> Vs \<inter> Vt \<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. thesis
[PROOF STEP]
using \<open>a \<in> R\<close> \<open>b \<in> R\<close> \<open>f \<in> R\<close> \<open>g \<in> R\<close> that
[PROOF STATE]
proof (prove)
using this:
is_zariski_open (Vs \<inter> Vt)
Vs \<inter> Vt \<subseteq> U
\<pp> \<in> Vs \<inter> Vt
?\<qq>3 \<in> Vs \<inter> Vt \<Longrightarrow> f \<notin> ?\<qq>3 \<and> s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> a f
?\<qq>3 \<in> Vs \<inter> Vt \<Longrightarrow> g \<notin> ?\<qq>3 \<and> t ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> b g
a \<in> R
b \<in> R
f \<in> R
g \<in> R
\<lbrakk>is_zariski_open ?V3; ?V3 \<subseteq> U; \<pp> \<in> ?V3; ?a3 \<in> R; ?f3 \<in> R; ?b3 \<in> R; ?g3 \<in> R; ?f3 \<notin> \<pp>; ?g3 \<notin> \<pp>; \<And>\<qq>. \<qq> \<in> ?V3 \<Longrightarrow> ?f3 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?a3 ?f3; \<And>\<qq>. \<qq> \<in> ?V3 \<Longrightarrow> ?g3 \<notin> \<qq> \<and> t \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> ?b3 ?g3\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed