[STATEMENT]
lemma ind_sheaf_is_presheaf:
  shows "presheaf_of_rings U (it.ind_is_open) ind_sheaf ind_ring_morphisms b
ind_add_str ind_mult_str ind_zero_str ind_one_str"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
have "topological_space U it.ind_is_open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. topological_space U it.ind_is_open
[PROOF STEP]
by (simp add: it.ind_space_is_top_space)
[PROOF STATE]
proof (state)
this:
topological_space U it.ind_is_open

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
topological_space U it.ind_is_open

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
have "ring_homomorphism (ind_ring_morphisms W V)
                     (ind_sheaf W) (ind_add_str W) (ind_mult_str W) (ind_zero_str W) (ind_one_str W)
                     (ind_sheaf V) (ind_add_str V) (ind_mult_str V) (ind_zero_str V) (ind_one_str V)"
    if "it.ind_is_open W" "it.ind_is_open V" "V \<subseteq> W" for W V
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_mult_str W) (ind_zero_str W) (ind_one_str W) (local.ind_sheaf V) (ind_add_str V) (ind_mult_str V) (ind_zero_str V) (ind_one_str V)
[PROOF STEP]
proof (intro ring_homomorphism.intro ind_is_open_imp_ring)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. Set_Theory.map (ind_ring_morphisms W V) (local.ind_sheaf W) (local.ind_sheaf V)
 2. it.ind_is_open W
 3. it.ind_is_open V
 4. group_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_zero_str W) (local.ind_sheaf V) (ind_add_str V) (ind_zero_str V)
 5. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
show "Set_Theory.map (ind_ring_morphisms W V) (ind_sheaf W) (ind_sheaf V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (ind_ring_morphisms W V) (local.ind_sheaf W) (local.ind_sheaf V)
[PROOF STEP]
unfolding ind_ring_morphisms_def ind_sheaf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (\<rho> (U \<inter> W) (U \<inter> V)) (\<FF> (U \<inter> W)) (\<FF> (U \<inter> V))
[PROOF STEP]
by (metis that it.ind_is_open_def inf.left_idem is_open_subset is_ring_morphism
          open_inter ring_homomorphism_def)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (ind_ring_morphisms W V) (local.ind_sheaf W) (local.ind_sheaf V)

goal (4 subgoals):
 1. it.ind_is_open W
 2. it.ind_is_open V
 3. group_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_zero_str W) (local.ind_sheaf V) (ind_add_str V) (ind_zero_str V)
 4. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
it.ind_is_open W
it.ind_is_open V
V \<subseteq> W
[PROOF STEP]
obtain o: "is_open (U \<inter> V)" "is_open (U \<inter> W)" "U \<inter> V \<subseteq> U \<inter> W"
[PROOF STATE]
proof (prove)
using this:
it.ind_is_open W
it.ind_is_open V
V \<subseteq> W

goal (1 subgoal):
 1. (\<lbrakk>is_open (U \<inter> V); is_open (U \<inter> W); U \<inter> V \<subseteq> U \<inter> W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types) it.ind_is_open_def inf.absorb_iff2 is_open_subset open_inter)
[PROOF STATE]
proof (state)
this:
is_open (U \<inter> V)
is_open (U \<inter> W)
U \<inter> V \<subseteq> U \<inter> W

goal (4 subgoals):
 1. it.ind_is_open W
 2. it.ind_is_open V
 3. group_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_zero_str W) (local.ind_sheaf V) (ind_add_str V) (ind_zero_str V)
 4. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open (U \<inter> V)
is_open (U \<inter> W)
U \<inter> V \<subseteq> U \<inter> W
[PROOF STEP]
show "group_homomorphism (ind_ring_morphisms W V) (ind_sheaf W) (ind_add_str W) (ind_zero_str W) (ind_sheaf V) (ind_add_str V) (ind_zero_str V)"
[PROOF STATE]
proof (prove)
using this:
is_open (U \<inter> V)
is_open (U \<inter> W)
U \<inter> V \<subseteq> U \<inter> W

goal (1 subgoal):
 1. group_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_zero_str W) (local.ind_sheaf V) (ind_add_str V) (ind_zero_str V)
[PROOF STEP]
unfolding ind_ring_morphisms_def ind_sheaf_def ind_zero_str_def
[PROOF STATE]
proof (prove)
using this:
is_open (U \<inter> V)
is_open (U \<inter> W)
U \<inter> V \<subseteq> U \<inter> W

goal (1 subgoal):
 1. group_homomorphism (\<rho> (U \<inter> W) (U \<inter> V)) (\<FF> (U \<inter> W)) (ind_add_str W) \<zero>\<^bsub>U \<inter> W\<^esub> (\<FF> (U \<inter> V)) (ind_add_str V) \<zero>\<^bsub>U \<inter> V\<^esub>
[PROOF STEP]
by (metis ind_sheaf.ind_add_str_def ind_sheaf_axioms is_ring_morphism ring_homomorphism.axioms(4))
[PROOF STATE]
proof (state)
this:
group_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_add_str W) (ind_zero_str W) (local.ind_sheaf V) (ind_add_str V) (ind_zero_str V)

goal (3 subgoals):
 1. it.ind_is_open W
 2. it.ind_is_open V
 3. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
show "monoid_homomorphism (ind_ring_morphisms W V) (ind_sheaf W) (ind_mult_str W) (ind_one_str W) (ind_sheaf V) (ind_mult_str V) (ind_one_str V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
using o
[PROOF STATE]
proof (prove)
using this:
is_open (U \<inter> V)
is_open (U \<inter> W)
U \<inter> V \<subseteq> U \<inter> W

goal (1 subgoal):
 1. monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)
[PROOF STEP]
by (metis ind_mult_str_def ind_one_str_def ind_ring_morphisms_def ind_sheaf_def is_ring_morphism ring_homomorphism_def)
[PROOF STATE]
proof (state)
this:
monoid_homomorphism (ind_ring_morphisms W V) (local.ind_sheaf W) (ind_mult_str W) (ind_one_str W) (local.ind_sheaf V) (ind_mult_str V) (ind_one_str V)

goal (2 subgoals):
 1. it.ind_is_open W
 2. it.ind_is_open V
[PROOF STEP]
qed (use that in auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>it.ind_is_open ?W1; it.ind_is_open ?V1; ?V1 \<subseteq> ?W1\<rbrakk> \<Longrightarrow> ring_homomorphism (ind_ring_morphisms ?W1 ?V1) (local.ind_sheaf ?W1) (ind_add_str ?W1) (ind_mult_str ?W1) (ind_zero_str ?W1) (ind_one_str ?W1) (local.ind_sheaf ?V1) (ind_add_str ?V1) (ind_mult_str ?V1) (ind_zero_str ?V1) (ind_one_str ?V1)

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>it.ind_is_open ?W1; it.ind_is_open ?V1; ?V1 \<subseteq> ?W1\<rbrakk> \<Longrightarrow> ring_homomorphism (ind_ring_morphisms ?W1 ?V1) (local.ind_sheaf ?W1) (ind_add_str ?W1) (ind_mult_str ?W1) (ind_zero_str ?W1) (ind_one_str ?W1) (local.ind_sheaf ?V1) (ind_add_str ?V1) (ind_mult_str ?V1) (ind_zero_str ?V1) (ind_one_str ?V1)

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
have "ind_sheaf {} = {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ind_sheaf {} = {b}
[PROOF STEP]
by (simp add: ring_of_empty ind_sheaf_def)
[PROOF STATE]
proof (state)
this:
local.ind_sheaf {} = {b}

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.ind_sheaf {} = {b}

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
have "\<And>U. it.ind_is_open U \<Longrightarrow> (\<And>x. x \<in> (ind_sheaf U) \<Longrightarrow> ind_ring_morphisms U U x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. it.ind_is_open U \<Longrightarrow> (\<And>x. x \<in> local.ind_sheaf U \<Longrightarrow> ind_ring_morphisms U U x = x)
[PROOF STEP]
by (simp add: Int_absorb1 it.ind_is_open_def ind_ring_morphisms_def ind_sheaf_def it.is_open_from_ind_is_open is_open_subset)
[PROOF STATE]
proof (state)
this:
\<lbrakk>it.ind_is_open ?U1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?U1 ?x1 = ?x1

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>it.ind_is_open ?U1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?U1 ?x1 = ?x1

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
have "\<And>U V W. it.ind_is_open U \<Longrightarrow> it.ind_is_open V \<Longrightarrow> it.ind_is_open W \<Longrightarrow> V \<subseteq> U \<Longrightarrow> W \<subseteq> V
             \<Longrightarrow> (\<And>x. x \<in> (ind_sheaf U) \<Longrightarrow> ind_ring_morphisms U W x = (ind_ring_morphisms V W \<circ> ind_ring_morphisms U V) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V W. \<lbrakk>it.ind_is_open U; it.ind_is_open V; it.ind_is_open W; V \<subseteq> U; W \<subseteq> V\<rbrakk> \<Longrightarrow> (\<And>x. x \<in> local.ind_sheaf U \<Longrightarrow> ind_ring_morphisms U W x = (ind_ring_morphisms V W \<circ> ind_ring_morphisms U V) x)
[PROOF STEP]
by (metis Int_absorb1 assoc_comp it.ind_is_open_def ind_ring_morphisms_def ind_sheaf_def it.is_open_from_ind_is_open is_open_subset)
[PROOF STATE]
proof (state)
this:
\<lbrakk>it.ind_is_open ?U1; it.ind_is_open ?V1; it.ind_is_open ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?W1 ?x1 = (ind_ring_morphisms ?V1 ?W1 \<circ> ind_ring_morphisms ?U1 ?V1) ?x1

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
topological_space U it.ind_is_open
\<lbrakk>it.ind_is_open ?W1; it.ind_is_open ?V1; ?V1 \<subseteq> ?W1\<rbrakk> \<Longrightarrow> ring_homomorphism (ind_ring_morphisms ?W1 ?V1) (local.ind_sheaf ?W1) (ind_add_str ?W1) (ind_mult_str ?W1) (ind_zero_str ?W1) (ind_one_str ?W1) (local.ind_sheaf ?V1) (ind_add_str ?V1) (ind_mult_str ?V1) (ind_zero_str ?V1) (ind_one_str ?V1)
local.ind_sheaf {} = {b}
\<lbrakk>it.ind_is_open ?U1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?U1 ?x1 = ?x1
\<lbrakk>it.ind_is_open ?U1; it.ind_is_open ?V1; it.ind_is_open ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?W1 ?x1 = (ind_ring_morphisms ?V1 ?W1 \<circ> ind_ring_morphisms ?U1 ?V1) ?x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
topological_space U it.ind_is_open
\<lbrakk>it.ind_is_open ?W1; it.ind_is_open ?V1; ?V1 \<subseteq> ?W1\<rbrakk> \<Longrightarrow> ring_homomorphism (ind_ring_morphisms ?W1 ?V1) (local.ind_sheaf ?W1) (ind_add_str ?W1) (ind_mult_str ?W1) (ind_zero_str ?W1) (ind_one_str ?W1) (local.ind_sheaf ?V1) (ind_add_str ?V1) (ind_mult_str ?V1) (ind_zero_str ?V1) (ind_one_str ?V1)
local.ind_sheaf {} = {b}
\<lbrakk>it.ind_is_open ?U1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?U1 ?x1 = ?x1
\<lbrakk>it.ind_is_open ?U1; it.ind_is_open ?V1; it.ind_is_open ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?W1 ?x1 = (ind_ring_morphisms ?V1 ?W1 \<circ> ind_ring_morphisms ?U1 ?V1) ?x1

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
unfolding presheaf_of_rings_def presheaf_of_rings_axioms_def
[PROOF STATE]
proof (prove)
using this:
topological_space U it.ind_is_open
\<lbrakk>it.ind_is_open ?W1; it.ind_is_open ?V1; ?V1 \<subseteq> ?W1\<rbrakk> \<Longrightarrow> ring_homomorphism (ind_ring_morphisms ?W1 ?V1) (local.ind_sheaf ?W1) (ind_add_str ?W1) (ind_mult_str ?W1) (ind_zero_str ?W1) (ind_one_str ?W1) (local.ind_sheaf ?V1) (ind_add_str ?V1) (ind_mult_str ?V1) (ind_zero_str ?V1) (ind_one_str ?V1)
local.ind_sheaf {} = {b}
\<lbrakk>it.ind_is_open ?U1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?U1 ?x1 = ?x1
\<lbrakk>it.ind_is_open ?U1; it.ind_is_open ?V1; it.ind_is_open ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> local.ind_sheaf ?U1\<rbrakk> \<Longrightarrow> ind_ring_morphisms ?U1 ?W1 ?x1 = (ind_ring_morphisms ?V1 ?W1 \<circ> ind_ring_morphisms ?U1 ?V1) ?x1

goal (1 subgoal):
 1. topological_space U it.ind_is_open \<and> ((\<forall>U V. it.ind_is_open U \<longrightarrow> it.ind_is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> ring_homomorphism (ind_ring_morphisms U V) (local.ind_sheaf U) (ind_add_str U) (ind_mult_str U) (ind_zero_str U) (ind_one_str U) (local.ind_sheaf V) (ind_add_str V) (ind_mult_str V) (ind_zero_str V) (ind_one_str V)) \<and> local.ind_sheaf {} = {b}) \<and> (\<forall>U. it.ind_is_open U \<longrightarrow> (\<forall>x. x \<in> local.ind_sheaf U \<longrightarrow> ind_ring_morphisms U U x = x)) \<and> (\<forall>U V W. it.ind_is_open U \<longrightarrow> it.ind_is_open V \<longrightarrow> it.ind_is_open W \<longrightarrow> V \<subseteq> U \<longrightarrow> W \<subseteq> V \<longrightarrow> (\<forall>x. x \<in> local.ind_sheaf U \<longrightarrow> ind_ring_morphisms U W x = (ind_ring_morphisms V W \<circ> ind_ring_morphisms U V) x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_sheaf_is_sheaf:
  shows "sheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 3. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
show "presheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
using ind_sheaf_is_presheaf
[PROOF STATE]
proof (prove)
using this:
presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str

goal (1 subgoal):
 1. presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
presheaf_of_rings U it.ind_is_open local.ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str

goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
fix V I W s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
    and WV: "\<And>i. i \<in> I \<Longrightarrow> W i \<subseteq> V"
    and s: "s \<in> ind_sheaf V"
    and eq: "\<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms V (W i) s = ind_zero_str (W i)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset U it.ind_is_open V I W
?i1 \<in> I \<Longrightarrow> W ?i1 \<subseteq> V
s \<in> local.ind_sheaf V
?i1 \<in> I \<Longrightarrow> ind_ring_morphisms V (W ?i1) s = ind_zero_str (W ?i1)

goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "it.ind_is_open V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it.ind_is_open V
[PROOF STEP]
using oc open_cover_of_open_subset.is_open_subset
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset U it.ind_is_open V I W
open_cover_of_open_subset ?X ?is_open ?U ?I ?C \<Longrightarrow> ?is_open ?U

goal (1 subgoal):
 1. it.ind_is_open V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
it.ind_is_open V

goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
it.ind_is_open V
[PROOF STEP]
have "s \<in> \<FF> V"
[PROOF STATE]
proof (prove)
using this:
it.ind_is_open V

goal (1 subgoal):
 1. s \<in> \<FF> V
[PROOF STEP]
by (metis ind_sheaf.ind_sheaf_def ind_sheaf_axioms it.ind_is_open_def inf.absorb2 s)
[PROOF STATE]
proof (state)
this:
s \<in> \<FF> V

goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<FF> V
[PROOF STEP]
have "s = \<zero>\<^bsub>V\<^esub>"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<FF> V

goal (1 subgoal):
 1. s = \<zero>\<^bsub>V\<^esub>
[PROOF STEP]
by (metis Int_absorb1 Int_subset_iff WV ind_sheaf.ind_zero_str_def ind_sheaf_axioms eq it.ind_is_open_def ind_ring_morphisms_def is_open_subset locality oc it.open_cover_from_ind_open_cover open_cover_of_open_subset.is_open_subset)
[PROOF STATE]
proof (state)
this:
s = \<zero>\<^bsub>V\<^esub>

goal (2 subgoals):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> Ua; s \<in> local.ind_sheaf Ua; \<And>i. i \<in> I \<Longrightarrow> ind_ring_morphisms Ua (V i) s = ind_zero_str (V i)\<rbrakk> \<Longrightarrow> s = ind_zero_str Ua
 2. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = \<zero>\<^bsub>V\<^esub>
[PROOF STEP]
show "s = ind_zero_str V"
[PROOF STATE]
proof (prove)
using this:
s = \<zero>\<^bsub>V\<^esub>

goal (1 subgoal):
 1. s = ind_zero_str V
[PROOF STEP]
by (metis Int_absorb1 it.ind_is_open_def ind_zero_str_def oc open_cover_of_open_subset.is_open_subset)
[PROOF STATE]
proof (state)
this:
s = ind_zero_str V

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
fix V I W s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
    and WV: "\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> ind_sheaf (W i)"
    and eq: "\<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (W i) (W i \<inter> W j) (s i) = ind_ring_morphisms (W j) (W i \<inter> W j) (s j)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset U it.ind_is_open V I W
\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> local.ind_sheaf (W i)
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = ind_ring_morphisms (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "is_open V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_open V
[PROOF STEP]
using it.is_open_from_ind_is_open is_open_subset oc open_cover_of_open_subset.is_open_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open U; it.ind_is_open ?U\<rbrakk> \<Longrightarrow> is_open ?U
is_open U
open_cover_of_open_subset U it.ind_is_open V I W
open_cover_of_open_subset ?X ?is_open ?U ?I ?C \<Longrightarrow> ?is_open ?U

goal (1 subgoal):
 1. is_open V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_open V

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_open V

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "open_cover_of_open_subset S is_open V I W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open_cover_of_open_subset S is_open V I W
[PROOF STEP]
using it.open_cover_from_ind_open_cover oc ind_topology.intro ind_topology_axioms_def is_open_subset it.is_subset topological_space_axioms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open U; open_cover_of_open_subset U it.ind_is_open ?U ?I ?C\<rbrakk> \<Longrightarrow> open_cover_of_open_subset S is_open ?U ?I ?C
open_cover_of_open_subset U it.ind_is_open V I W
\<lbrakk>topological_space ?X ?is_open; ind_topology_axioms ?X ?S\<rbrakk> \<Longrightarrow> ind_topology ?X ?is_open ?S
ind_topology_axioms ?X ?S \<equiv> ?S \<subseteq> ?X
is_open U
U \<subseteq> S
topological_space S is_open

goal (1 subgoal):
 1. open_cover_of_open_subset S is_open V I W
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S is_open V I W

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S is_open V I W

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "\<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)"
    if "i\<in>I" "j\<in>I" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)
[PROOF STEP]
have "U \<inter> W i = W i" and "U \<inter> W j = W j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<inter> W i = W i &&& U \<inter> W j = W j
[PROOF STEP]
by (metis Int_absorb1 WV it.ind_is_open_def oc open_cover_of_open_subset.is_open_subset
            subset_trans that)+
[PROOF STATE]
proof (state)
this:
U \<inter> W i = W i
U \<inter> W j = W j

goal (1 subgoal):
 1. \<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<inter> W i = W i
U \<inter> W j = W j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
U \<inter> W i = W i
U \<inter> W j = W j

goal (1 subgoal):
 1. \<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)
[PROOF STEP]
using eq[unfolded ind_ring_morphisms_def,OF that]
[PROOF STATE]
proof (prove)
using this:
U \<inter> W i = W i
U \<inter> W j = W j
\<rho> (U \<inter> W i) (U \<inter> (W i \<inter> W j)) (s i) = \<rho> (U \<inter> W j) (U \<inter> (W i \<inter> W j)) (s j)

goal (1 subgoal):
 1. \<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)
[PROOF STEP]
by (metis inf_sup_aci(2))
[PROOF STATE]
proof (state)
this:
\<rho> (W i) (W i \<inter> W j) (s i) = \<rho> (W j) (W i \<inter> W j) (s j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = \<rho> (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = \<rho> (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "\<forall>i. i\<in>I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)
[PROOF STEP]
by (metis WV it.ind_is_open_def ind_sheaf_def inf.orderE inf_idem inf_aci(3) oc open_cover_of_open_subset.is_open_subset)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_open V
open_cover_of_open_subset S is_open V I W
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = \<rho> (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)
\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)
[PROOF STEP]
obtain t where "t \<in> (\<FF> V) \<and> (\<forall>i. i\<in>I \<longrightarrow> \<rho> V (W i) t = s i)"
[PROOF STATE]
proof (prove)
using this:
is_open V
open_cover_of_open_subset S is_open V I W
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = \<rho> (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)
\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)

goal (1 subgoal):
 1. (\<And>t. t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using glueing
[PROOF STATE]
proof (prove)
using this:
is_open V
open_cover_of_open_subset S is_open V I W
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (W ?i1) (W ?i1 \<inter> W ?j1) (s ?i1) = \<rho> (W ?j1) (W ?i1 \<inter> W ?j1) (s ?j1)
\<forall>i. i \<in> I \<longrightarrow> W i \<subseteq> V \<and> s i \<in> \<FF> (W i)
\<lbrakk>open_cover_of_open_subset S is_open ?U ?I ?V; \<forall>i. i \<in> ?I \<longrightarrow> ?V i \<subseteq> ?U \<and> ?s i \<in> \<FF> (?V i); \<And>i j. \<lbrakk>i \<in> ?I; j \<in> ?I\<rbrakk> \<Longrightarrow> \<rho> (?V i) (?V i \<inter> ?V j) (?s i) = \<rho> (?V j) (?V i \<inter> ?V j) (?s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> \<FF> ?U \<and> (\<forall>i. i \<in> ?I \<longrightarrow> \<rho> ?U (?V i) t = ?s i)

goal (1 subgoal):
 1. (\<And>t. t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)
[PROOF STEP]
have "t \<in> ind_sheaf V"
[PROOF STATE]
proof (prove)
using this:
t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)

goal (1 subgoal):
 1. t \<in> local.ind_sheaf V
[PROOF STEP]
unfolding ind_sheaf_def
[PROOF STATE]
proof (prove)
using this:
t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)

goal (1 subgoal):
 1. t \<in> \<FF> (U \<inter> V)
[PROOF STEP]
using oc
[PROOF STATE]
proof (prove)
using this:
t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)
open_cover_of_open_subset U it.ind_is_open V I W

goal (1 subgoal):
 1. t \<in> \<FF> (U \<inter> V)
[PROOF STEP]
by (metis Int_absorb1 cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
[PROOF STATE]
proof (state)
this:
t \<in> local.ind_sheaf V

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<in> local.ind_sheaf V

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
have "\<forall>i. i\<in>I \<longrightarrow> ind_ring_morphisms V (W i) t = s i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms V (W i) t = s i
[PROOF STEP]
unfolding ind_ring_morphisms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> I \<longrightarrow> \<rho> (U \<inter> V) (U \<inter> W i) t = s i
[PROOF STEP]
by (metis oc Int_absorb1 \<open>t \<in> \<FF> V \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> V (W i) t = s i)\<close> cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms V (W i) t = s i

goal (1 subgoal):
 1. \<And>Ua I V s. \<lbrakk>open_cover_of_open_subset U it.ind_is_open Ua I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> Ua \<and> s i \<in> local.ind_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> ind_ring_morphisms (V i) (V i \<inter> V j) (s i) = ind_ring_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.ind_sheaf Ua \<and> (\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms Ua (V i) t = s i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t \<in> local.ind_sheaf V
\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms V (W i) t = s i
[PROOF STEP]
show "\<exists>t. t \<in> (ind_sheaf V) \<and> (\<forall>i. i\<in>I \<longrightarrow> ind_ring_morphisms V (W i) t = s i)"
[PROOF STATE]
proof (prove)
using this:
t \<in> local.ind_sheaf V
\<forall>i. i \<in> I \<longrightarrow> ind_ring_morphisms V (W i) t = s i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma im_sheaf_is_presheaf:
  "presheaf_of_rings S' (is_open') im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
proof (intro presheaf_of_rings.intro presheaf_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. topological_space S' is_open'
 2. \<And>U V. \<lbrakk>is_open' U; is_open' V; V \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms U V) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (local.im_sheaf V) (add_im_sheaf V) (mult_im_sheaf V) (zero_im_sheaf V) (one_im_sheaf V)
 3. local.im_sheaf {} = {b}
 4. \<And>U x. \<lbrakk>is_open' U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U U x = x
 5. \<And>U V W x. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "topological_space S' is_open'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. topological_space S' is_open'
[PROOF STEP]
by (simp add: target.topological_space_axioms)
[PROOF STATE]
proof (state)
this:
topological_space S' is_open'

goal (4 subgoals):
 1. \<And>U V. \<lbrakk>is_open' U; is_open' V; V \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms U V) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (local.im_sheaf V) (add_im_sheaf V) (mult_im_sheaf V) (zero_im_sheaf V) (one_im_sheaf V)
 2. local.im_sheaf {} = {b}
 3. \<And>U x. \<lbrakk>is_open' U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U U x = x
 4. \<And>U V W x. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "\<And>U V. \<lbrakk>is_open' U; is_open' V; V \<subseteq> U\<rbrakk>
           \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms U V)
(im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U)
(im_sheaf V) (add_im_sheaf V) (mult_im_sheaf V) (zero_im_sheaf V) (one_im_sheaf V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V. \<lbrakk>is_open' U; is_open' V; V \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms U V) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (local.im_sheaf V) (add_im_sheaf V) (mult_im_sheaf V) (zero_im_sheaf V) (one_im_sheaf V)
[PROOF STEP]
unfolding add_im_sheaf_def mult_im_sheaf_def zero_im_sheaf_def one_im_sheaf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V. \<lbrakk>is_open' U; is_open' V; V \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms U V) (local.im_sheaf U) +\<^bsub>f \<^sup>\<inverse> S U\<^esub> \<cdot>\<^bsub>f \<^sup>\<inverse> S U\<^esub> \<zero>\<^bsub>f \<^sup>\<inverse> S U\<^esub> \<one>\<^bsub>f \<^sup>\<inverse> S U\<^esub> (local.im_sheaf V) +\<^bsub>f \<^sup>\<inverse> S V\<^esub> \<cdot>\<^bsub>f \<^sup>\<inverse> S V\<^esub> \<zero>\<^bsub>f \<^sup>\<inverse> S V\<^esub> \<one>\<^bsub>f \<^sup>\<inverse> S V\<^esub>
[PROOF STEP]
by (metis Int_commute Int_mono im_sheaf_def im_sheaf_morphisms_def is_continuous is_ring_morphism subset_refl vimage_mono)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open' ?U1; is_open' ?V1; ?V1 \<subseteq> ?U1\<rbrakk> \<Longrightarrow> ring_homomorphism (im_sheaf_morphisms ?U1 ?V1) (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1) (local.im_sheaf ?V1) (add_im_sheaf ?V1) (mult_im_sheaf ?V1) (zero_im_sheaf ?V1) (one_im_sheaf ?V1)

goal (3 subgoals):
 1. local.im_sheaf {} = {b}
 2. \<And>U x. \<lbrakk>is_open' U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U U x = x
 3. \<And>U V W x. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "im_sheaf {} = {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.im_sheaf {} = {b}
[PROOF STEP]
using im_sheaf_def ring_of_empty
[PROOF STATE]
proof (prove)
using this:
local.im_sheaf ?V \<equiv> \<FF> (f \<^sup>\<inverse> S ?V)
\<FF> {} = {b}

goal (1 subgoal):
 1. local.im_sheaf {} = {b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.im_sheaf {} = {b}

goal (2 subgoals):
 1. \<And>U x. \<lbrakk>is_open' U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U U x = x
 2. \<And>U V W x. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "\<And>U. is_open' U \<Longrightarrow> (\<And>x. x \<in> (im_sheaf U) \<Longrightarrow> im_sheaf_morphisms U U x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open' U \<Longrightarrow> (\<And>x. x \<in> local.im_sheaf U \<Longrightarrow> im_sheaf_morphisms U U x = x)
[PROOF STEP]
using im_sheaf_morphisms_def
[PROOF STATE]
proof (prove)
using this:
im_sheaf_morphisms ?U ?V \<equiv> \<rho> (f \<^sup>\<inverse> S ?U) (f \<^sup>\<inverse> S ?V)

goal (1 subgoal):
 1. \<And>U. is_open' U \<Longrightarrow> (\<And>x. x \<in> local.im_sheaf U \<Longrightarrow> im_sheaf_morphisms U U x = x)
[PROOF STEP]
by (simp add: im_sheaf_def is_continuous)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open' ?U1; ?x1 \<in> local.im_sheaf ?U1\<rbrakk> \<Longrightarrow> im_sheaf_morphisms ?U1 ?U1 ?x1 = ?x1

goal (1 subgoal):
 1. \<And>U V W x. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "\<And>U V W.
       \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V\<rbrakk>
       \<Longrightarrow> (\<And>x. x \<in> (im_sheaf U) \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V W. \<lbrakk>is_open' U; is_open' V; is_open' W; V \<subseteq> U; W \<subseteq> V\<rbrakk> \<Longrightarrow> (\<And>x. x \<in> local.im_sheaf U \<Longrightarrow> im_sheaf_morphisms U W x = (im_sheaf_morphisms V W \<circ> im_sheaf_morphisms U V) x)
[PROOF STEP]
by (metis Int_mono assoc_comp im_sheaf_def im_sheaf_morphisms_def ind_topology.is_subset is_continuous ind_topology_is_open_self vimage_mono)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open' ?U1; is_open' ?V1; is_open' ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> local.im_sheaf ?U1\<rbrakk> \<Longrightarrow> im_sheaf_morphisms ?U1 ?W1 ?x1 = (im_sheaf_morphisms ?V1 ?W1 \<circ> im_sheaf_morphisms ?U1 ?V1) ?x1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma im_sheaf_is_sheaf:
  shows "sheaf_of_rings S' (is_open') im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 3. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
show "presheaf_of_rings S' is_open' im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
using im_sheaf_is_presheaf
[PROOF STATE]
proof (prove)
using this:
presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf

goal (1 subgoal):
 1. presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
presheaf_of_rings S' is_open' local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_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 S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_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 S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
assume oc: "open_cover_of_open_subset S' is_open' U I V"
    and VU: "\<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U"
    and s: "s \<in> im_sheaf U"
    and eq0: "\<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s =zero_im_sheaf (V i)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S' is_open' U I V
?i1 \<in> I \<Longrightarrow> V ?i1 \<subseteq> U
s \<in> local.im_sheaf U
?i1 \<in> I \<Longrightarrow> im_sheaf_morphisms U (V ?i1) s = zero_im_sheaf (V ?i1)

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
have "open_cover_of_open_subset S is_open (f\<^sup>\<inverse> S U) I (\<lambda>i. f\<^sup>\<inverse> S (V i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
[PROOF STEP]
by (simp add: oc open_cover_of_open_subset_from_target_to_source)
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))

goal (2 subgoals):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U; s \<in> local.im_sheaf U; \<And>i. i \<in> I \<Longrightarrow> im_sheaf_morphisms U (V i) s = zero_im_sheaf (V i)\<rbrakk> \<Longrightarrow> s = zero_im_sheaf U
 2. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
[PROOF STEP]
show "s = zero_im_sheaf U"
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))

goal (1 subgoal):
 1. s = zero_im_sheaf U
[PROOF STEP]
using zero_im_sheaf_def
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
zero_im_sheaf \<equiv> \<lambda>V. \<zero>\<^bsub>f \<^sup>\<inverse> S V\<^esub>

goal (1 subgoal):
 1. s = zero_im_sheaf U
[PROOF STEP]
by (smt VU im_sheaf_def im_sheaf_morphisms_def eq0 inf.absorb_iff2 inf_le2 inf_sup_aci(1) inf_sup_aci(3) locality s vimage_Int)
[PROOF STATE]
proof (state)
this:
s = zero_im_sheaf U

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_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 S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_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 S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
assume oc: "open_cover_of_open_subset S' is_open' U I V"
    and VU: "\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> im_sheaf (V i)"
    and eq: "\<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)"
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S' is_open' U I V
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i)
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V ?i1) (V ?i1 \<inter> V ?j1) (s ?i1) = im_sheaf_morphisms (V ?j1) (V ?i1 \<inter> V ?j1) (s ?j1)

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
have "\<exists>t. t \<in> \<FF> (f  \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f  \<^sup>\<inverse> S U) (f  \<^sup>\<inverse> S (V i)) t = s i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)
[PROOF STEP]
proof (rule glueing)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
 2. \<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))
 3. \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> \<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)
[PROOF STEP]
show "open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
[PROOF STEP]
using oc open_cover_of_open_subset_from_target_to_source
[PROOF STATE]
proof (prove)
using this:
open_cover_of_open_subset S' is_open' U I V
open_cover_of_open_subset S' is_open' ?U ?I ?C \<Longrightarrow> open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S ?U) ?I (\<lambda>i. f \<^sup>\<inverse> S (?C i))

goal (1 subgoal):
 1. open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
open_cover_of_open_subset S is_open (f \<^sup>\<inverse> S U) I (\<lambda>i. f \<^sup>\<inverse> S (V i))

goal (2 subgoals):
 1. \<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))
 2. \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> \<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)
[PROOF STEP]
show "\<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))
[PROOF STEP]
using VU im_sheaf_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i)
local.im_sheaf ?V \<equiv> \<FF> (f \<^sup>\<inverse> S ?V)

goal (1 subgoal):
 1. \<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> I \<longrightarrow> f \<^sup>\<inverse> S (V i) \<subseteq> f \<^sup>\<inverse> S U \<and> s i \<in> \<FF> (f \<^sup>\<inverse> S (V i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> \<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)
[PROOF STEP]
show "\<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)"
      if "i \<in> I" "j \<in> I" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)
[PROOF STEP]
using im_sheaf_morphisms_def eq that
[PROOF STATE]
proof (prove)
using this:
im_sheaf_morphisms ?U ?V \<equiv> \<rho> (f \<^sup>\<inverse> S ?U) (f \<^sup>\<inverse> S ?V)
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V ?i1) (V ?i1 \<inter> V ?j1) (s ?i1) = im_sheaf_morphisms (V ?j1) (V ?i1 \<inter> V ?j1) (s ?j1)
i \<in> I
j \<in> I

goal (1 subgoal):
 1. \<rho> (f \<^sup>\<inverse> S (V i)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s i) = \<rho> (f \<^sup>\<inverse> S (V j)) (f \<^sup>\<inverse> S (V i) \<inter> f \<^sup>\<inverse> S (V j)) (s j)
[PROOF STEP]
by (smt Int_commute Int_left_commute inf.left_idem vimage_Int)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 \<in> I; ?j1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (f \<^sup>\<inverse> S (V ?i1)) (f \<^sup>\<inverse> S (V ?i1) \<inter> f \<^sup>\<inverse> S (V ?j1)) (s ?i1) = \<rho> (f \<^sup>\<inverse> S (V ?j1)) (f \<^sup>\<inverse> S (V ?i1) \<inter> f \<^sup>\<inverse> S (V ?j1)) (s ?j1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t. t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)
[PROOF STEP]
obtain t where "t \<in> \<FF> (f\<^sup>\<inverse> S U) \<and> (\<forall>i. i\<in>I \<longrightarrow> \<rho> (f\<^sup>\<inverse> S U) (f\<^sup>\<inverse> S (V i)) t = s i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)

goal (1 subgoal):
 1. (\<And>t. t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)

goal (1 subgoal):
 1. \<And>U I V s. \<lbrakk>open_cover_of_open_subset S' is_open' U I V; \<forall>i. i \<in> I \<longrightarrow> V i \<subseteq> U \<and> s i \<in> local.im_sheaf (V i); \<And>i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> im_sheaf_morphisms (V i) (V i \<inter> V j) (s i) = im_sheaf_morphisms (V j) (V i \<inter> V j) (s j)\<rbrakk> \<Longrightarrow> \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)
[PROOF STEP]
show "\<exists>t. t \<in> im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)"
[PROOF STATE]
proof (prove)
using this:
t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)

goal (1 subgoal):
 1. \<exists>t. t \<in> local.im_sheaf U \<and> (\<forall>i. i \<in> I \<longrightarrow> im_sheaf_morphisms U (V i) t = s i)
[PROOF STEP]
using im_sheaf_def im_sheaf_morphisms_def
[PROOF STATE]
proof (prove)
using this:
t \<in> \<FF> (f \<^sup>\<inverse> S U) \<and> (\<forall>i. i \<in> I \<longrightarrow> \<rho> (f \<^sup>\<inverse> S U) (f \<^sup>\<inverse> S (V i)) t = s i)
local.im_sheaf ?V \<equiv> \<FF> (f \<^sup>\<inverse> S ?V)
im_sheaf_morphisms ?U ?V \<equiv> \<rho> (f \<^sup>\<inverse> S ?U) (f \<^sup>\<inverse> S ?V)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in sheaf_of_rings) id_to_iso_of_sheaves:
  shows "iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            (im_sheaf.im_sheaf S \<FF> (identity S))
            (im_sheaf.im_sheaf_morphisms S \<rho> (identity S))
            b
            (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))"
    (is "iso_sheaves_of_rings S is_open \<FF> \<rho> b _ _ _ _ _ _ b  ?add ?mult ?zero ?one ?F")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (im_sheaf.im_sheaf S \<FF> (identity S)) (im_sheaf.im_sheaf_morphisms S \<rho> (identity S)) b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (im_sheaf.im_sheaf S \<FF> (identity S)) (im_sheaf.im_sheaf_morphisms S \<rho> (identity S)) b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have preq[simp]: "\<And>V. V \<subseteq> S \<Longrightarrow> (identity S \<^sup>\<inverse> S V) = V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V. V \<subseteq> S \<Longrightarrow> identity S \<^sup>\<inverse> S V = V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?V1 \<subseteq> S \<Longrightarrow> identity S \<^sup>\<inverse> S ?V1 = ?V1

goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (im_sheaf.im_sheaf S \<FF> (identity S)) (im_sheaf.im_sheaf_morphisms S \<rho> (identity S)) b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
interpret id: im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open "identity S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open (identity S)
[PROOF STEP]
by intro_locales (auto simp add: Set_Theory.map_def continuous_map_axioms_def open_imp_subset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have 1[simp]: "\<And>V. V \<subseteq> S \<Longrightarrow> im_sheaf.im_sheaf S \<FF> (identity S) V = \<FF> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V. V \<subseteq> S \<Longrightarrow> id.im_sheaf V = \<FF> V
[PROOF STEP]
by (simp add: id.im_sheaf_def)
[PROOF STATE]
proof (state)
this:
?V1 \<subseteq> S \<Longrightarrow> id.im_sheaf ?V1 = \<FF> ?V1

goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have 2[simp]: "\<And>U V. \<lbrakk>U \<subseteq> S; V \<subseteq> S\<rbrakk> \<Longrightarrow> im_sheaf.im_sheaf_morphisms S \<rho> (identity S) U V \<equiv> \<rho> U V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V. \<lbrakk>U \<subseteq> S; V \<subseteq> S\<rbrakk> \<Longrightarrow> id.im_sheaf_morphisms U V \<equiv> \<rho> U V
[PROOF STEP]
using id.im_sheaf_morphisms_def
[PROOF STATE]
proof (prove)
using this:
id.im_sheaf_morphisms ?U ?V \<equiv> \<rho> (identity S \<^sup>\<inverse> S ?U) (identity S \<^sup>\<inverse> S ?V)

goal (1 subgoal):
 1. \<And>U V. \<lbrakk>U \<subseteq> S; V \<subseteq> S\<rbrakk> \<Longrightarrow> id.im_sheaf_morphisms U V \<equiv> \<rho> U V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?U1 \<subseteq> S; ?V1 \<subseteq> S\<rbrakk> \<Longrightarrow> id.im_sheaf_morphisms ?U1 ?V1 \<equiv> \<rho> ?U1 ?V1

goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
 2. morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
 3. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have rh: "\<And>U. is_open U \<Longrightarrow>
         ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
using id_is_mor_pr_rngs morphism_presheaves_of_rings.is_ring_morphism
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (?fam_morphisms ?U) (?\<FF> ?U) (?add_str ?U) (?mult_str ?U) (?zero_str ?U) (?one_str ?U) (?\<FF>' ?U) (?add_str' ?U) (?mult_str' ?U) (?zero_str' ?U) (?one_str' ?U)

goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub>

goal (3 subgoals):
 1. presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
 2. morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
 3. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str
           id.im_sheaf id.im_sheaf_morphisms ?add ?mult ?zero ?one ?F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (id.im_sheaf U) +\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<cdot>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<zero>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<one>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub>) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (id.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x))
[PROOF STEP]
by (auto simp: rh open_imp_subset intro: is_map_from_is_homomorphism map.map_closed)
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))

goal (2 subgoals):
 1. presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
 2. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have \<rho>: "\<And>U V W x. \<lbrakk>is_open U; is_open V; is_open W; V \<subseteq> U; W \<subseteq> V; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> \<rho> V W (\<rho> U V x) = \<rho> U W x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V W x. \<lbrakk>is_open U; is_open V; is_open W; V \<subseteq> U; W \<subseteq> V; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> \<rho> V W (\<rho> U V x) = \<rho> U W x
[PROOF STEP]
by (metis assoc_comp comp_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open ?U1; is_open ?V1; is_open ?W1; ?V1 \<subseteq> ?U1; ?W1 \<subseteq> ?V1; ?x1 \<in> \<FF> ?U1\<rbrakk> \<Longrightarrow> \<rho> ?V1 ?W1 (\<rho> ?U1 ?V1 ?x1) = \<rho> ?U1 ?W1 ?x1

goal (2 subgoals):
 1. presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
 2. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
[PROOF STEP]
by (auto simp: \<rho> presheaf_of_rings_axioms_def is_ring_morphism open_imp_subset ring_of_empty)
[PROOF STATE]
proof (state)
this:
presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)

goal (1 subgoal):
 1. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
[PROOF STEP]
have "presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
[PROOF STATE]
proof (prove)
using this:
presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)

goal (1 subgoal):
 1. presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
[PROOF STEP]
by (metis id.im_sheaf_is_presheaf presheaf_of_rings_def)
[PROOF STATE]
proof (state)
this:
presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)

goal (1 subgoal):
 1. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)

goal (1 subgoal):
 1. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have "morphism_presheaves_of_rings_axioms is_open
          id.im_sheaf id.im_sheaf_morphisms ?add ?mult ?zero ?one \<FF> \<rho> add_str
          mult_str zero_str one_str (\<lambda>U. \<lambda>x\<in>\<FF> U. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) \<FF> \<rho> add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (id.im_sheaf U) +\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<cdot>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<zero>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<one>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> id.im_sheaf U \<longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> id.im_sheaf_morphisms U V) x))
[PROOF STEP]
by (auto simp: rh open_imp_subset intro: is_map_from_is_homomorphism map.map_closed)
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) \<FF> \<rho> add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
morphism_presheaves_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) \<FF> \<rho> add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one ?F"
[PROOF STATE]
proof (prove)
using this:
presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>)
morphism_presheaves_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) \<FF> \<rho> add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (auto simp: presheaf_of_rings_axioms iso_presheaves_of_rings_axioms_def morphism_presheaves_of_rings_def open_imp_subset)
[PROOF STATE]
proof (state)
this:
iso_presheaves_of_rings_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iso_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str id.im_sheaf id.im_sheaf_morphisms b (\<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cancel_imp_equal:
  "\<lbrakk> u \<cdot> inverse v = \<one>;  u \<in> G; v \<in> G \<rbrakk> \<Longrightarrow> u = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<cdot> local.inverse v = \<one>; u \<in> G; v \<in> G\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
by (metis invertible invertible_inverse_closed invertible_right_cancel invertible_right_inverse)


[STATEMENT]
lemma inverse_distributive: "\<lbrakk> a \<in> R; b \<in> R; c \<in> R \<rbrakk> \<Longrightarrow> a \<cdot> (b - c) = a \<cdot> b - a \<cdot> c"
    "\<lbrakk> a \<in> R; b \<in> R; c \<in> R \<rbrakk> \<Longrightarrow> (b - c) \<cdot> a = b \<cdot> a - c \<cdot> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> a \<cdot> (b - c) = a \<cdot> b - a \<cdot> c) &&& (\<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> (b - c) \<cdot> a = b \<cdot> a - c \<cdot> a)
[PROOF STEP]
using additive.invertible additive.invertible_inverse_closed distributive
        local.left_minus local.right_minus
[PROOF STATE]
proof (prove)
using this:
?u \<in> R \<Longrightarrow> additive.invertible ?u
\<lbrakk>additive.invertible ?u; ?u \<in> R\<rbrakk> \<Longrightarrow> - ?u \<in> R
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> (?b + ?c) \<cdot> ?a = ?b \<cdot> ?a + ?c \<cdot> ?a
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> (- ?a) \<cdot> ?b = - ?a \<cdot> ?b
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (- ?b) = - ?a \<cdot> ?b

goal (1 subgoal):
 1. (\<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> a \<cdot> (b - c) = a \<cdot> b - a \<cdot> c) &&& (\<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> (b - c) \<cdot> a = b \<cdot> a - c \<cdot> a)
[PROOF STEP]
by presburger+


[STATEMENT]
lemma rel_refl: "\<And>x. x \<in> R \<times> S \<Longrightarrow> x \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> R \<times> S \<Longrightarrow> x \<sim> x
[PROOF STEP]
by (auto simp: rel_def)