(*  Title:      bpl/Basic_Perturbation_Lemma_local_nilpot.thy
    ID:         $Id: Basic_Perturbation_Lemma_local_nilpot.thy $
    Author:     Jesus Aransay
    Comments:
*)

header{*Proof of the Basic Perturbation Lemma*}

theory Basic_Perturbation_Lemma_local_nilpot 
  imports 
  lemma_2_2_19_local_nilpot
  begin

text{*In the following locale we define an abbreviation that we will use later in proofs, and we also join the results obtained in locale
  @{text "lemma_2_2_17"} with the ones reached in @{text "lemma_2_2_11"}. The combination of both locales give us the set of premises in the 
  Basic Perturbation Lemma (from now on, BPL) statement*}

locale BPL = lemma_2_2_17 + lemma_2_2_11

context BPL
begin

definition f' where "f' == (completion 
  \<lparr>carrier = kernel D D p, mult = op \<otimes>, one = \<one>, 
  diff = completion \<lparr>carrier = kernel D D p, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> D (differ)\<rparr> C f)"

end

lemma (in BPL) \<pi>_gf: shows "g \<circ> f = \<pi>"
proof -
  let ?gf = "g \<circ> f" 
    (*We have to use this abbreviation ?gf because, otherwise, Isabelle complained about the type of expression "g \<otimes>\<^bsub>R\<^esub> f \<in> carrier R"*)
  from g_f_hom_diff have "?gf \<in> hom_completion D D" unfolding hom_diff_def by simp
  with ring_R have gf_in_R: "?gf \<in> carrier R" by simp
  from gf_dh_hd and ring_R have "?gf \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ) = \<one>\<^bsub>R\<^esub>" by simp
  then have "?gf \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ) \<ominus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ) = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)" by simp
  with gf_in_R and R.one_closed and diff_in_R and h_in_R have "?gf = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)" by algebra
  with \<pi>_def and p_def and ring_R show "g \<circ> f = \<pi>" by simp
qed

subsection{*BPL proof*}

text{*The following lemma corresponds to the first part of @{text "Lemma 2.2.20"} (i.e., the BPL) in Aransay's memoir*}
text{*The proof of the BPL is divided into two parts, as it is also in Aransay's memoir. *}
text{*In the first part, proved in @{text "BPL_reduction"}, from the given premises, we buid a new reduction 
  from @{text "D' = \<lparr> carrier = carrier D, \<dots>, diff = differ\<^bsub>D\<^esub> \<oplus>\<^bsub>R\<^esub> \<delta>\<rparr>"} into @{text C'}, 
  where @{text "C' = \<lparr> carrier = carrier C, \<dots> , diff = f' \<circ> (\<tau>' \<circ>  differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g\<rparr> (f' \<circ> (\<tau>' \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')))"} *}
text{*The reduction is given by the triple @{term [locale=BPL] "f' \<circ> (\<tau>' \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p'))"}, @{term [locale=BPL] "(inc_ker_p' \<circ> \<tau> \<circ> g)"}, 
  @{term [locale=BPL] "h'"}*}
text{*In the second part of the proof of the BPL, here stored in lemma @{text "BPL_simplifications"}, 
  the expressions @{term [locale=BPL] "f' \<circ> (\<tau>' \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p'))"}, @{term [locale=BPL] "(inc_ker_p' \<circ> \<tau> \<circ> g)"}
   and @{term [locale=BPL] "f' \<circ> (\<tau>' \<circ>  differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g"} are simplified, obtaining the ones in the BPL statement*}
text{*By finally joining @{text "BPL_reduction"} and @{text "BPL_simplifications"}, we complete the proof of the BPL*}

subsection{*Existence of a reduction*}

lemma (in BPL) BPL_reduction:
  shows "reduction D'
  \<lparr> carrier = carrier C, mult = mult C, one = one C, diff = f' \<circ> (\<tau>' \<circ>  differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g\<rparr> (f' \<circ> (\<tau>' \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p'))) 
  (inc_ker_p' \<circ> \<tau> \<circ> g) h'"
proof -
    (*The following shows a way to import in our context the lemmas in locale "reduction"*)
    (*from reduction_D_C interpret reduction [D C f g h] by (rule reduction.axioms)+*)
    (*from reduction_D_C interpret lemma_2_2_11 [D C f g h] by simp*)
  
    (*First reduction:*)
  from lemma_2_2_15 have red_D'_ker_p': " reduction D' diff_group_ker_p' (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') inc_ker_p' h'" by simp
  
  have iso_inv_diff_ker_p'_ker_p: 
    "(\<tau>', \<tau>) \<in> diff_group_ker_p' \<cong>\<^bsub>invdiff\<^esub>  \<lparr> carrier = kernel D D p, mult = mult D, one = one D, diff = \<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>\<rparr>"
    (is "(\<tau>', \<tau>) \<in> diff_group_ker_p' \<cong>\<^bsub>invdiff\<^esub>  ?ker_p_pert")
      and diff_group_ker_p_pert: "diff_group  \<lparr> carrier = kernel D D p, mult = mult D, one = one D, diff = \<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>\<rparr>"
    (is "diff_group ?ker_p_pert")
  proof -
    from lemma_2_2_17 have iso_inv_compl: "(\<tau>', \<tau>) \<in> diff_group_ker_p' \<cong>\<^bsub>invcompl\<^esub> diff_group_ker_p" unfolding iso_inv_compl_def by simp
    from lemma_2_2_15 have diff_group_ker_p': "diff_group diff_group_ker_p'" unfolding reduction_def diff_group_def by simp
    from lemma_2_2_14 have comm_group_ker_p: "comm_group diff_group_ker_p" unfolding reduction_def diff_group_def comm_group_def by simp
    from lemma_2_2_18 [OF diff_group_ker_p' comm_group_ker_p iso_inv_compl]
    show "(\<tau>', \<tau>) \<in> diff_group_ker_p' \<cong>\<^bsub>invdiff\<^esub>  ?ker_p_pert" and "diff_group ?ker_p_pert" 
      unfolding diff_group_ker_p_def by simp_all
  qed
  
  (*Second reduction:*)
  from reduction.lemma_2_2_19 [OF red_D'_ker_p' diff_group_ker_p_pert iso_inv_diff_ker_p'_ker_p]
  have red_D'_ker_p_pert: "reduction D' ?ker_p_pert (\<tau>' \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')) (inc_ker_p' \<circ> \<tau>) h'" by simp
  
  (*Now we prove the premises for defining the third and last reduction*)
  have ker_p_isom_C: "(f', g) \<in> (diff_group_ker_p \<cong>\<^bsub>invdiff\<^esub> C)"
  proof -
    from iso_inv_diff_rev [OF lemma_2_2_11] have im_gf_isom_C: "(completion diff_group_im_gf C f, g) \<in> (diff_group_im_gf \<cong>\<^bsub>invdiff\<^esub> C)" by simp
    moreover from \<pi>_gf have "g \<circ> f = \<pi>" by simp
    moreover from im_\<pi>_ker_p have im_\<pi>_ker_p: "\<pi> ` carrier D = kernel D D p" by simp
    ultimately show ?thesis unfolding diff_group_im_gf_def im_gf_def diff_group_ker_p_def f'_def by simp
  qed
  then have ker_p_pert_isom_C: "(f', g) \<in> (?ker_p_pert \<cong>\<^bsub>invcompl\<^esub> C)"
    unfolding iso_inv_diff_def iso_inv_compl_def diff_group_ker_p_def iso_diff_def iso_compl_def hom_diff_def hom_completion_def
      hom_def Pi_def completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
  from red_D'_ker_p_pert have diff_group_ker_p_pert: "diff_group ?ker_p_pert" unfolding reduction_def diff_group_def by simp
  from C_diff_group have C: "comm_group C" unfolding diff_group_def comm_group_def by simp
  from lemma_2_2_18 [OF diff_group_ker_p_pert C ker_p_pert_isom_C]
  have f'_g_isom: "(f', g) \<in> (?ker_p_pert \<cong>\<^bsub>invdiff\<^esub> 
    \<lparr> carrier = carrier C, mult = op \<otimes>\<^bsub>C\<^esub>, one = \<one>\<^bsub>C\<^esub>, diff = f' \<circ>  (\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g\<rparr>)" 
    (is "(f', g) \<in> (?ker_p_pert \<cong>\<^bsub>invdiff\<^esub> ?C')")
      and diff_group_C_pert: 
      "diff_group \<lparr>carrier = carrier C, mult = op \<otimes>\<^bsub>C\<^esub>, one = \<one>\<^bsub>C\<^esub>, diff = f' \<circ>  (\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g \<rparr>"
    (is "diff_group ?C'") by simp_all
  
  (*Third reduction*)
  from reduction.lemma_2_2_19 [OF red_D'_ker_p_pert diff_group_C_pert f'_g_isom]
  show "reduction D' ?C' (f' \<circ> (\<tau>' \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')) (inc_ker_p' \<circ> \<tau> \<circ> g) h'" by simp
qed

subsection{*BPL previous simplifications*}

text{*In order to prove the simplifications required in the second part of the proof, i.e. lemma @{text "BPL_simplifications"}, 
  we first have to prove some results concerning the composition of some of the homomorphisms and endomorphisms we have already introduced.*}
text{*Therefore, we have the ring @{term [locale=ring_endomorphisms] "R"}
  and we prove that it behaves as expected with some homomorphisms from @{text "Hom (D C)"} and @{text "Hom (C D)"}, 
  where the operation to relate them is the composition*}
text{*We will prove some properties such as distributivity of composition with respect to addition of endomorphisms and the like*}
text{*The results are stated in generic terms*}

lemma (in ring_endomorphisms) add_dist_comp: assumes C: "diff_group C" and g: "g \<in> hom_completion C D" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" shows "(a \<oplus>\<^bsub>R\<^esub> b) \<circ> g = (\<lambda>x. if x \<in> carrier C then (a \<circ> g) x \<otimes> (b \<circ> g) x else \<one>)"
  using ring_R and g and a and b and hom_completion_closed [OF g] and completion_closed2 [of g C D] and group_hom.hom_one [of D D a]
    group_hom.hom_one [of D D b] and D_diff_group
  unfolding hom_completion_def completion_def diff_group_def comm_group_def group_hom_def group_hom_axioms_def
  by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) comp_hom_compl: assumes C: "diff_group C" and g: "g \<in> hom_completion C D" and a: "a \<in> carrier R"
  shows "a \<circ> g = (\<lambda>x. if x \<in> carrier C then (a \<circ> g) x else \<one>)"
  using ring_R and g and a and hom_completion_closed [OF g] and completion_closed2 [of g C D] 
    and group_hom.hom_one [of D D a] and D_diff_group
  unfolding hom_completion_def completion_def diff_group_def comm_group_def group_hom_def group_hom_axioms_def
  by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) one_comp_g: assumes C: "diff_group C" and g: "g \<in> hom_completion C D"
  shows "\<one>\<^bsub>R\<^esub> \<circ> g = g"
  using ring_R and g and hom_completion_closed [OF g] and completion_closed2 [of g C D]
  unfolding hom_completion_def completion_fun2_def completion_def apply simp by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) minus_dist_comp: assumes C: "diff_group C" and g: "g \<in> hom_completion C D" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" shows "(a \<ominus>\<^bsub>R\<^esub> b) \<circ> g = (\<lambda>x. if x \<in> carrier C then (a \<circ> g) x \<otimes> ((\<ominus>\<^bsub>R\<^esub> b) \<circ> g) x else \<one>)"
  using add_dist_comp [OF C g a a_inv_closed [OF b]] unfolding a_minus_def [OF a b] by simp

lemma (in ring_endomorphisms) minus_comp_g: assumes C: "diff_group C" and g: "g \<in> hom_completion C D" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" and a_eq_b: "a = b" shows "(\<ominus>\<^bsub>R\<^esub> a) \<circ> g = (\<ominus>\<^bsub>R\<^esub> b) \<circ> g"
proof -
  from a and b and a_eq_b have "\<ominus>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> b" by algebra
  then show ?thesis by simp
qed

lemma (in ring_endomorphisms) minus_comp_g2: assumes C: "diff_group C" and g: "g \<in> hom_completion C D" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" and a_eq_b: "a \<circ> g = b \<circ> g" shows "(\<ominus>\<^bsub>R\<^esub> a) \<circ> g =  (\<ominus>\<^bsub>R\<^esub> b) \<circ> g"
  using a_eq_b and minus_interpret [OF a] minus_interpret [OF b] and g by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_add_dist_comp: includes diff_group C assumes f: "f \<in> hom_completion D C" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" shows "f \<circ> (a \<oplus>\<^bsub>R\<^esub> b) = (\<lambda>x. if x \<in> carrier D then (f \<circ> a) x \<otimes>\<^bsub>C\<^esub> (f \<circ> b) x else \<one>\<^bsub>C\<^esub>)"
  using prems ring_R and f and a and b and hom_completion_closed [of a D D] hom_completion_closed [of b D D]
    and hom_completion_mult [of f D C] group_hom.hom_one [of D C f] and D.diff_group_is_group C.diff_group_is_group
 unfolding hom_completion_def [of D C] group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_comp_hom_compl: assumes C: "diff_group C" and f: "f \<in> hom_completion D C" and a: "a \<in> carrier R"
  shows "f \<circ> a = (\<lambda>x. if x \<in> carrier D then (f \<circ> a) x else \<one>\<^bsub>C\<^esub>)"
  using ring_R and f and a and hom_completion_closed [of a] and completion_closed2 [of a D D] and group_hom.hom_one [of D C f] and C 
    and D_diff_group
  unfolding diff_group_def comm_group_def hom_completion_def group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_minus_dist_comp: includes diff_group C assumes f: "f \<in> hom_completion D C" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" shows "f \<circ> (a \<ominus>\<^bsub>R\<^esub> b) = (\<lambda>x. if x \<in> carrier D then (f \<circ> a) x \<otimes>\<^bsub>C\<^esub> (f \<circ> (\<ominus>\<^bsub>R\<^esub> b)) x else \<one>\<^bsub>C\<^esub>)"
  using l_add_dist_comp [OF _ f a a_inv_closed [OF b]] unfolding a_minus_def [OF a b] by (simp add: prems)

(*The following result turned to be much harder than the previous version in the right hand:
  whereas a = b implies directly that - a \<circ> f = - b \<circ> f (proved in lemma minus_comp_g2), when proving a = b implies f (- a) = f (- b)
  the problem appears that the "inv" definition does not have to be coherent with f, i.e. f (inv a x) \<noteq> inv (f a x). 
  We propose a proof where the commutative group hom_completion D C is introduced, and using that the inverse is unique in this group,
  and also that f \<circ> a, f \<circ> b, f \<circ> (- a) and f \<circ> (- b) are elements of such a ring, the proof is possible*)

lemma (in ring_endomorphisms) l_minus_comp_f: assumes C: "diff_group C" and f: "f \<in> hom_completion D C" and a: "a \<in> carrier R"
  and b: "b \<in> carrier R" and a_eq_b: "f \<circ> a = f \<circ> b" shows "f \<circ> (\<ominus>\<^bsub>R\<^esub> a) =  f \<circ> (\<ominus>\<^bsub>R\<^esub> b)"
proof -
  from HomGroupsCompletion.hom_completion_groups_mult_comm_group [of D C] and C and D_diff_group
  have Hom_D_C: "comm_group \<lparr>carrier = hom_completion D C, mult = \<lambda>f g x. if x \<in> carrier D then f x \<otimes>\<^bsub>C\<^esub> g x else \<one>\<^bsub>C\<^esub>,
         one = \<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>\<rparr>" unfolding diff_group_def comm_group_def by simp
  let ?hom_D_C = "\<lparr>carrier = hom_completion D C, mult = \<lambda>f g x. if x \<in> carrier D then f x \<otimes>\<^bsub>C\<^esub> g x else \<one>\<^bsub>C\<^esub>,
         one = \<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>\<rparr>"
  from ring_R and group_hom.hom_one [of D C f] and f and C and D_diff_group have one_fzero: "one ?hom_D_C = f \<circ> \<zero>\<^bsub>R\<^esub>"
    unfolding diff_group_def comm_group_def group_def hom_completion_def group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)
  also from R.r_neg [OF a] have "\<dots> = f \<circ> (a \<oplus>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> a)" by simp
  also from l_add_dist_comp [OF C f a a_inv_closed [OF a]] have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> a) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> a) x else \<one>\<^bsub>C\<^esub>)"
    by simp
  also from a_eq_b have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> b) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> a) x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  also from Hom_D_C have "\<dots> = (f \<circ> b) \<otimes>\<^bsub>?hom_D_C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> a)" by simp
  finally have fb_f_minus_a: "one ?hom_D_C = (f \<circ> b) \<otimes>\<^bsub>?hom_D_C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> a)" by simp
  from one_fzero have "one ?hom_D_C = f \<circ> \<zero>\<^bsub>R\<^esub>" by simp
  also from R.l_neg [OF b] have "\<dots> = f \<circ> (\<ominus>\<^bsub>R\<^esub> b \<oplus>\<^bsub>R\<^esub> b)" by simp
  also from l_add_dist_comp [OF C f a_inv_closed [OF b] b] and Hom_D_C have "\<dots> = (f \<circ> \<ominus>\<^bsub>R\<^esub> b) \<otimes>\<^bsub>?hom_D_C\<^esub> (f \<circ> b)" by simp
  finally have f_minus_b_fb: "one ?hom_D_C = (f \<circ> \<ominus>\<^bsub>R\<^esub> b) \<otimes>\<^bsub>?hom_D_C\<^esub> (f \<circ> b)" by simp
  from monoid.inv_unique [of ?hom_D_C "(f \<circ> \<ominus>\<^bsub>R\<^esub> b)" "f \<circ> b" "(f \<circ> \<ominus>\<^bsub>R\<^esub> a)"] and a_inv_closed [OF a] b a_inv_closed [OF b] 
    and sym [OF f_minus_b_fb] and sym [OF fb_f_minus_a] and ring_R 
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C "\<ominus>\<^bsub>R\<^esub> a" f]
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C b f] 
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C "\<ominus>\<^bsub>R\<^esub> b" f]
    and C and D_diff_group and f and Hom_D_C
  show "(f \<circ> \<ominus>\<^bsub>R\<^esub> a) = (f \<circ> \<ominus>\<^bsub>R\<^esub> b)" unfolding diff_group_def comm_group_def group_def by simp
qed

text{*The following properties are used later in lemma @{text "BPL_simplifications"}; just in order to make the proof of 
  @{text "BPL_simplification"} shorter, we  have extracted them, as far as they are not generic properties that can 
  be used in other different settings*}

lemma (in BPL) inc_ker_p\<tau>_eq_\<tau>: shows "inc_ker_p' \<circ> \<tau> = \<tau>"
proof -
  have "image \<tau> (\<pi> ` carrier D) \<subseteq> kernel D' D' p'"
  proof (unfold image_def \<tau>_def, auto)
    fix x assume x: "x \<in> carrier D" with \<pi>_in_R and ring_R and hom_completion_closed [of \<pi> D D x] have "\<pi> x  \<in> carrier D" by simp
    with im_\<pi>_ker_p and D'_def show "\<pi>' (\<pi> x) \<in> kernel D' D' p'" unfolding image_def by auto
  qed
  with inc_ker_p'_def and \<tau>_def and D'_def show "inc_ker_p' \<circ> \<tau> = \<tau>" unfolding completion_def expand_fun_eq by auto
qed

lemma (in BPL) \<tau>g_eq_\<pi>'g: shows "\<tau> \<circ> g = \<pi>' \<circ> g"
proof -
  from \<pi>_gf have im_g_im_\<pi>: "image g (carrier C)  \<subseteq> \<pi>` carrier D"
  proof (unfold image_def, auto simp add: expand_fun_eq)
    fix x assume x: "x \<in> carrier C" with fg have fg_x: "f (g x) = x" by (simp add: expand_fun_eq)
    with hom_diff_closed [OF g_hom_diff x] have "g (f (g x)) = g x" and "g x \<in> carrier D" by (simp_all)
    with \<pi>_gf show "\<exists>y\<in>carrier D. g x = \<pi> (y)" by (force simp add: expand_fun_eq)
  qed
  show "\<tau> \<circ> g = \<pi>' \<circ> g" 
  proof (rule ext)
    fix x
    show "(\<tau> \<circ> g) x = (\<pi>' \<circ> g) x"
    proof (cases "x \<in> carrier C")
      case True with im_g_im_\<pi> and \<tau>_def and g_hom_diff show "(\<tau> \<circ> g) x = (\<pi>' \<circ> g) x"
	unfolding completion_def hom_diff_def hom_completion_def hom_def Pi_def by (auto simp add: expand_fun_eq)
    next
      case False with g_hom_diff and completion_closed2 [of g C D x] have g_x: "g x = \<one>\<^bsub>D\<^esub>"
	unfolding hom_diff_def hom_completion_def by simp
      with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p diff_group_ker_p' \<tau>] and lemma_2_2_14 and lemma_2_2_15
      have r_h_s: "\<tau> (g x) = \<one>\<^bsub>D\<^esub>"
	unfolding reduction_def diff_group_def comm_group_def group_def 
	unfolding \<tau>_def iso_inv_compl_def iso_compl_def diff_group_ker_p_def diff_group_ker_p'_def by simp
      from C_diff_group D_diff_group and g_x and \<pi>'_in_R and ring_R and hom_completion_one [of D D \<pi>']
      have l_h_s: "\<pi>' (g x) = \<one>\<^bsub>D\<^esub>" unfolding diff_group_def comm_group_def group_def by simp
      from r_h_s and l_h_s show "(\<tau> \<circ> g) x = (\<pi>' \<circ> g) x" by simp
    qed
  qed
qed

lemma (in BPL) diff'h'g_eq_zero: shows "(diff' \<otimes>\<^bsub>R\<^esub> h') \<circ> g = (\<lambda>x. if x \<in> carrier C then \<one> else \<one>)"
proof -
  from ring_R have "(diff' \<otimes>\<^bsub>R\<^esub> h') \<circ> g = (diff' \<circ> h') \<circ> g" by simp
  also have "\<dots> = diff' \<circ> (h' \<circ> g)" by (simp add: o_assoc)
  also from h'_def and psi_h_h_phi and ring_R have "\<dots> = diff' \<circ> ((\<Psi> \<circ> h) \<circ> g)" by simp
  also have "\<dots> = diff' \<circ> (\<Psi> \<circ> (h \<circ> g))" by (simp add: o_assoc)
  also from hg have "\<dots> = diff' \<circ> (\<Psi> \<circ> (\<lambda>x. if x \<in> carrier C then \<one> else \<one>))" by simp
  also from psi_in_R and diff'_in_R and ring_R and hom_completion_one [of D D diff'] hom_completion_one [of D D \<Psi>] 
    and C_diff_group and D_diff_group
  have "\<dots> = (\<lambda>x. if x \<in> carrier C then \<one> else \<one>)" unfolding diff_group_def comm_group_def group_def by (simp add: expand_fun_eq)
  finally show ?thesis by simp
qed

lemma (in BPL) h'diff'g_eq_psihdeltag: shows "(h' \<otimes>\<^bsub>R\<^esub> diff') \<circ> g = (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g"
proof -
  from ring_R and sym [OF o_assoc [of h' diff' g]] have "(h' \<otimes>\<^bsub>R\<^esub> diff') \<circ> g = h' \<circ> (diff' \<circ> g)" by simp
  also from add_dist_comp [of C g differ \<delta>] and diff'_def and diff_in_R and pert_in_R and C_diff_group and g_hom_diff
  have "\<dots> = h' \<circ> (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>D\<^esub> \<circ> g) x \<otimes>\<^bsub>D\<^esub> (\<delta> \<circ> g) x else \<one>)" unfolding hom_diff_def by simp
  also from hom_diff_coherent [OF g_hom_diff] 
  have "\<dots> = h' \<circ> (\<lambda>x. if x \<in> carrier C then (g \<circ> differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>D\<^esub> (\<delta> \<circ> g) x else \<one>)" by (simp add: expand_fun_eq)
  also have "\<dots> = (\<lambda>x. if x \<in> carrier C then (h' \<circ> (g \<circ> differ\<^bsub>C\<^esub>)) x \<otimes> (h' \<circ> (\<delta> \<circ> g)) x else \<one>)"
  proof (auto simp add: expand_fun_eq)
    fix x assume x: "x \<in> carrier C"
    from ring_R and h'_in_R and hom_completion_mult [of h' D D "(g ((differ\<^bsub>C\<^esub>) x))" "\<delta> (g x)"]
      and hom_completion_closed [OF diff_group.diff_hom [OF C_diff_group] x] 
      and hom_diff_closed [OF g_hom_diff, of "(differ\<^bsub>C\<^esub>) x"]
      and hom_diff_closed [OF g_hom_diff x] and pert_in_R hom_completion_closed [of "\<delta>" D D "g x"]
    show "h' (g ((differ\<^bsub>C\<^esub>) x) \<otimes> \<delta> (g x)) = h' (g ((differ\<^bsub>C\<^esub>) x)) \<otimes> h' (\<delta> (g x))" by simp
  next
    from D.diff_group_is_group have D: "group D" by simp
    with ring_R and h'_in_R show "h' \<one> = \<one>" by (intro hom_completion_one, simp_all)
  qed
  also have "\<dots> =  (\<lambda>x. if x \<in> carrier C then (h' \<circ> g \<circ> differ\<^bsub>C\<^esub>) x \<otimes> (h' \<circ> (\<delta> \<circ> g)) x else \<one>)" by (simp add: expand_fun_eq o_assoc)
  also from h'_def and ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier C then (h \<circ> \<Phi> \<circ> g \<circ> differ\<^bsub>C\<^esub>) x \<otimes> (h \<circ> \<Phi> \<circ> (\<delta> \<circ> g)) x else \<one>)" 
    by (simp add: expand_fun_eq)
  also from psi_h_h_phi and ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<Psi> \<circ> h \<circ> g \<circ> differ\<^bsub>C\<^esub>) x \<otimes> (\<Psi> \<circ> h \<circ> (\<delta> \<circ> g)) x else \<one>)"
    by (simp add: expand_fun_eq)
  also have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<Psi> \<circ> h \<circ> (\<delta> \<circ> g)) x else \<one>)"
  proof (auto simp add: expand_fun_eq)
    fix x assume x: "x \<in> carrier C"
    from hg and psi_in_R and hom_completion_one [of D D \<Psi>] and ring_R and D.diff_group_is_group
    have " \<Psi> (h (g ((differ\<^bsub>C\<^esub>) x))) = \<one>" by (simp add: expand_fun_eq)
    moreover have "\<Psi> (h (\<delta> (g x))) \<in> carrier D"
    proof -
      from pert_in_R and h_in_R and psi_in_R have "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta> \<in> carrier R" by algebra
      with ring_R have psi_h_pert: "\<Psi> \<circ>  h \<circ> \<delta> \<in> hom_completion D D" by simp
      from hom_completion_closed [OF psi_h_pert, of "g x"] and hom_diff_closed [OF g_hom_diff x]
      show "\<Psi> (h (\<delta> (g x))) \<in> carrier D" by simp
    qed
    ultimately show "\<Psi> (h (g ((differ\<^bsub>C\<^esub>) x))) \<otimes> \<Psi> (h (\<delta> (g x))) = \<Psi> (h (\<delta> (g x)))" by (simp add: D.r_one)
  qed
  also from ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>  \<circ> g) x else \<one>)" by (simp add: expand_fun_eq)
  also from comp_hom_compl [of C g "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>"] and pert_in_R h_in_R psi_in_R and g_hom_diff C_diff_group
  have "\<dots> = (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g" unfolding hom_diff_def by simp
  finally show ?thesis by simp
qed

lemma (in BPL) p'g_eq_psihdeltag: shows "p' \<circ> g = (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g"
proof -
  from p'_def and ring_R and diff'_def have "p' \<circ> g = ((diff' \<otimes>\<^bsub>R\<^esub> h') \<oplus>\<^bsub>R\<^esub> (h' \<otimes>\<^bsub>R\<^esub> diff')) \<circ> g" by (simp add: expand_fun_eq)
  also from add_dist_comp [of C g "(diff' \<otimes>\<^bsub>R\<^esub> h')" "(h' \<otimes>\<^bsub>R\<^esub> diff')"] and g_hom_diff and diff'_in_R h'_in_R and C_diff_group
  have "\<dots> =  (\<lambda>x. if x \<in> carrier C then ((diff' \<otimes>\<^bsub>R\<^esub> h') \<circ> g) x \<otimes> ((h' \<otimes>\<^bsub>R\<^esub> diff') \<circ> g) x else \<one>)" by (unfold hom_diff_def, simp)
  also from diff'h'g_eq_zero and h'diff'g_eq_psihdeltag have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta> \<circ> g) x else \<one>)"
  proof (auto simp add: expand_fun_eq, intro D.l_one)
    fix x assume x: "x \<in> carrier C"
    from pert_in_R and h_in_R and psi_in_R have "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta> \<in> carrier R" by algebra
    with ring_R have psi_h_pert: "\<Psi> \<otimes>\<^bsub>R\<^esub>  h \<otimes>\<^bsub>R\<^esub> \<delta> \<in> hom_completion D D" by simp
    from hom_completion_closed [OF psi_h_pert, of "g x"] and hom_diff_closed [OF g_hom_diff x] 
    show "(\<Psi> \<otimes>\<^bsub>R\<^esub>  h \<otimes>\<^bsub>R\<^esub> \<delta>) (g x) \<in> carrier D" by simp
  qed
  also from comp_hom_compl [of C g "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>"] and pert_in_R h_in_R psi_in_R and g_hom_diff C_diff_group
  have "\<dots> = (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g" by (unfold hom_diff_def, simp)
  finally show ?thesis by simp
qed

lemma (in BPL) \<tau>'\<pi>'_eq_\<pi>\<pi>': shows "\<tau>' \<circ> \<pi>' = \<pi> \<circ> \<pi>'"
proof (rule ext)
  fix x
  show "(\<tau>' \<circ> \<pi>') x = (\<pi> \<circ> \<pi>') x"
  proof (cases "x \<in> carrier D")
    case True with \<pi>'_in_R ring_R and hom_completion_closed [of \<pi>' D D x] 
    have \<pi>'_im: "\<pi>' x \<in> \<pi>'`(carrier D)" and \<pi>'_D: "\<pi>' x \<in> carrier D" unfolding image_def by auto
    with \<tau>'_def and D'_def show "(\<tau>' \<circ> \<pi>') x = (\<pi> \<circ> \<pi>') x" by (simp add: expand_fun_eq)
  next
    case False with \<pi>'_in_R and ring_R and completion_closed2 [of \<pi>' D D x] have \<pi>'_x: "\<pi>' x = \<one>" unfolding hom_completion_def by simp
    with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p' diff_group_ker_p \<tau>'] and lemma_2_2_14 and lemma_2_2_15
    have r_h_s: "\<tau>' (\<pi>' x) = \<one>\<^bsub>D\<^esub>"
      unfolding reduction_def diff_group_def comm_group_def group_def \<tau>'_def 
      unfolding iso_inv_compl_def iso_compl_def diff_group_ker_p_def diff_group_ker_p'_def by simp
    from \<pi>_in_R and ring_R and hom_completion_one [of D D \<pi>] and \<pi>'_x and D.diff_group_is_group
    have l_h_s: "\<pi> (\<pi>' x) = \<one>" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) f'\<pi>_eq_f\<pi>: shows "f' \<circ> \<pi> = f \<circ> \<pi>"
proof (rule ext)
  fix x
  show "(f' \<circ> \<pi>) x = (f \<circ> \<pi>) x"
  proof (cases "x \<in> carrier D")
    case True with \<pi>_in_R and ring_R and hom_completion_closed [of \<pi> D D] have \<pi>_im: "\<pi> x \<in> \<pi>`(carrier D)" 
      and \<pi>_D: "\<pi> x \<in> carrier D" by (unfold image_def, auto)
    then have "\<pi> x \<in> kernel D D p" using im_\<pi>_ker_p by simp
    then show "(f' \<circ> \<pi>) x = (f \<circ> \<pi>) x" unfolding f'_def by (simp add: expand_fun_eq)
  next
    case False with \<pi>_in_R and ring_R and completion_closed2 [of \<pi> D D x] have \<pi>_x: "\<pi> x = \<one>" unfolding hom_completion_def by simp
    from iso_inv_diff_rev [OF lemma_2_2_11] and \<pi>_gf im_\<pi>_ker_p
    have "(f', g) \<in> (diff_group_im_gf \<cong>\<^bsub>invdiff\<^esub> C)" unfolding f'_def diff_group_im_gf_def im_gf_def by simp
    with hom_completion_one [of diff_group_im_gf C f'] and \<pi>_x and C.diff_group_is_group and image_g_f_diff_group 
    have r_h_s: "f' (\<pi> x) = \<one>\<^bsub>C\<^esub>" unfolding diff_group_im_gf_def im_gf_def diff_group_def comm_group_def 
      iso_inv_diff_def iso_diff_def hom_diff_def by simp
    from hom_diff_is_hom_completion [OF f_hom_diff] and hom_completion_one [of D C f] and \<pi>_x 
      and D.diff_group_is_group C.diff_group_is_group have l_h_s: "f (\<pi> x) = \<one>\<^bsub>C\<^esub>" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) f\<pi>_eq_f: shows "f \<circ> \<pi> = f"
proof -
  from sym [OF \<pi>_gf] have "f \<circ> \<pi> = f \<circ> g \<circ> f" by (simp add: o_assoc)
  also from fg have "\<dots> = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>) \<circ> f" by simp
  also from f_hom_diff have "\<dots> = f" 
    unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def by (auto simp add: expand_fun_eq)
  finally have "f \<circ> \<pi> = f" by simp
  then show ?thesis by (simp add: expand_fun_eq)
qed

lemma (in BPL) fh'diff'_eq_zero: shows "f \<circ> (h' \<otimes>\<^bsub>R\<^esub> diff') = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)"
proof -
  from ring_R have "f \<circ> (h' \<otimes>\<^bsub>R\<^esub> diff') = f \<circ> h' \<circ> diff'" by (simp add: o_assoc)
  also from ring_R and h'_def and o_assoc [of f h \<Phi>] have "\<dots> = f \<circ> h \<circ> \<Phi> \<circ> diff'" by simp
  also from fh have "\<dots> = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  finally show "f \<circ> (h' \<otimes>\<^bsub>R\<^esub> diff') = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)" by simp
qed

lemma (in BPL) fdiff'h'_eq_fdeltahphi: shows "f \<circ> (diff' \<otimes>\<^bsub>R\<^esub> h') = f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>"
proof -
  from diff'_def have "f \<circ> (diff' \<otimes>\<^bsub>R\<^esub> h') = f \<circ> (differ \<oplus>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> h'" by simp
  also from diff_in_R and pert_in_R and h'_in_R have "\<dots> = f \<circ> (differ \<otimes>\<^bsub>R\<^esub> h' \<oplus>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h')" by algebra
  also from l_add_dist_comp [OF C_diff_group, of f "differ \<otimes>\<^bsub>R\<^esub> h'" "\<delta> \<otimes>\<^bsub>R\<^esub> h'"] and diff_in_R and pert_in_R and h'_in_R and f_hom_diff
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> differ \<otimes>\<^bsub>R\<^esub> h') x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h') x else \<one>\<^bsub>C\<^esub>)" unfolding hom_diff_def by simp
  also from ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> differ \<circ> h') x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h') x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  also from hom_diff_coherent [OF f_hom_diff] 
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (differ\<^bsub>C\<^esub> \<circ> f \<circ> h') x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h') x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  also from h'_def and ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier D then (differ\<^bsub>C\<^esub> \<circ> f \<circ> h \<circ> \<Phi>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h') x else \<one>\<^bsub>C\<^esub>)" 
    by (simp add: expand_fun_eq)
  also from fh and hom_completion_one [OF _ _ diff_hom] C.diff_group_is_group and l_one and hom_completion_closed [of h' D D]
    and hom_completion_closed [of \<delta> D D] and hom_diff_closed [OF f_hom_diff] and ring_R and h'_in_R and pert_in_R
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h') x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  also from l_comp_hom_compl [OF C_diff_group, of f "\<delta> \<otimes>\<^bsub>R\<^esub> h'"] and f_hom_diff have "\<dots> = f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h'" unfolding hom_diff_def by simp
  also from h'_def and pert_in_R and h_in_R and phi_in_R have "\<dots> = f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>" by algebra
  finally show ?thesis by simp
qed

lemma (in BPL) fp'_eq_fdeltahphi: shows "f \<circ> p' = f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>"
proof -
  from p'_def and diff'_def and l_add_dist_comp [OF C_diff_group, of f "diff' \<otimes>\<^bsub>R\<^esub> h'" "h' \<otimes>\<^bsub>R\<^esub> diff'"] f_hom_diff 
    and diff'_in_R pert_in_R h'_in_R
  have "f \<circ> p' = (\<lambda>x. if x \<in> carrier D then (f \<circ> diff' \<otimes>\<^bsub>R\<^esub> h') x \<otimes>\<^bsub>C\<^esub> (f \<circ> h' \<otimes>\<^bsub>R\<^esub> diff') x else \<one>\<^bsub>C\<^esub>)" by (unfold hom_diff_def, simp)
  also from fh'diff'_eq_zero and fdiff'h'_eq_fdeltahphi and r_one and hom_completion_closed [of h D D] and hom_completion_closed [of \<Phi> D D]
    and hom_completion_closed [of \<delta> D D] and hom_diff_closed [OF f_hom_diff] and ring_R and h_in_R and phi_in_R and pert_in_R
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>) x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
  also from l_comp_hom_compl [OF C_diff_group, of f "\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>"] and h_in_R and phi_in_R and pert_in_R f_hom_diff
  have "\<dots> = f \<circ> \<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>" unfolding hom_diff_def by simp
  finally show ?thesis by simp
qed

lemma (in BPL) diff_ker_p'\<pi>'_eq_diff'\<pi>': shows "differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<pi>' = diff' \<circ> \<pi>'"
proof (rule ext)
  fix x
  show "(differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<pi>') x = (diff' \<circ> \<pi>') x"
  proof (cases "x \<in> carrier D")
    case True from im_\<pi>_ker_p and D'_def have im_\<pi>'_ker_p': "image \<pi>' (carrier D) \<subseteq> kernel D' D' p'" by simp
    with True show "(differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<pi>') x = (diff' \<circ> \<pi>') x"
      unfolding diff_group_ker_p'_def diff'_def D'_def completion_def image_def by (auto simp add: expand_fun_eq)
  next
    case False with \<pi>'_in_R and ring_R and completion_closed2 [of \<pi>' D D x] have \<pi>'_x: "\<pi>' x = \<one>" unfolding hom_completion_def by simp
    with diff'_in_R and ring_R and hom_completion_one [of D D diff'] and D.diff_group_is_group 
    have l_h_s: "(diff' \<circ> \<pi>') x = \<one>" by simp
    from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have diff_ker_p': "differ\<^bsub>diff_group_ker_p'\<^esub> \<in> hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    from \<pi>'_x and hom_completion_one [OF _ _ diff_ker_p'] and reduction.C_diff_group [OF lemma_2_2_15]
    have r_h_s: "(differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<pi>') x = \<one>" unfolding diff_group_ker_p'_def diff_group_def comm_group_def group_def by simp
    from l_h_s and r_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) \<tau>'diff'_eq_\<pi>diff': shows "\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> = \<pi> \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>"
proof (rule ext)
  fix x
  show "(\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>) x = (\<pi> \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>) x"
  proof (cases "x \<in> kernel D' D' p'")
    case True from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have "differ\<^bsub>diff_group_ker_p'\<^esub> \<in> hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    then have "image (differ\<^bsub>diff_group_ker_p'\<^esub>) (kernel D' D' p') \<subseteq> kernel D' D' p'"
      unfolding diff_group_ker_p'_def hom_completion_def hom_def Pi_def image_def kernel_def D'_def by auto
    with im_\<pi>_ker_p and D'_def have "image (differ\<^bsub>diff_group_ker_p'\<^esub>) (kernel D' D' p') \<subseteq> image \<pi>' (carrier D)" by simp
    with True and \<tau>'_def show "(\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>) x = (\<pi> \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>) x"
      unfolding completion_def image_def D'_def by (auto simp add: expand_fun_eq)
  next
    case False from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have "differ\<^bsub>diff_group_ker_p'\<^esub> \<in> hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    with completion_closed2 [of "differ\<^bsub>diff_group_ker_p'\<^esub>" diff_group_ker_p' diff_group_ker_p' x] and False and D'_def
    have diff'_x: "(differ\<^bsub>diff_group_ker_p'\<^esub>) x = \<one>" unfolding hom_completion_def diff_group_ker_p'_def by simp
    with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p' diff_group_ker_p \<tau>'] and lemma_2_2_14 and lemma_2_2_15
    have r_h_s: "\<tau>' ((differ\<^bsub>diff_group_ker_p'\<^esub>) x) = \<one>\<^bsub>D\<^esub>"
      unfolding reduction_def diff_group_def comm_group_def group_def \<tau>'_def iso_inv_compl_def iso_compl_def diff_group_ker_p_def 
	diff_group_ker_p'_def by simp
    from \<pi>_in_R and ring_R and hom_completion_one [of D D \<pi>] and diff'_x and D.diff_group_is_group
    have l_h_s: "\<pi> ((differ\<^bsub>diff_group_ker_p'\<^esub>) x) = \<one>" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) f\<pi>'g_eq_id: shows "f \<circ> \<pi>' \<circ> g = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)"
proof -
  have "f \<circ> \<pi>' \<circ> g = f \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') \<circ> g" unfolding \<pi>'_def by simp
  also from l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f p'] and p'_in_R and f_hom_diff and C_diff_group
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<one>\<^bsub>R\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> (\<ominus>\<^bsub>R\<^esub> p')) x else \<one>\<^bsub>C\<^esub>) \<circ> g" unfolding hom_diff_def by simp
  also from phi_in_R h_in_R pert_in_R and l_minus_comp_f [OF C_diff_group, of f p' "\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>"]  and fp'_eq_fdeltahphi and f_hom_diff
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<one>\<^bsub>R\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) x else \<one>\<^bsub>C\<^esub>) \<circ> g"
    unfolding hom_diff_def by (auto simp add: expand_fun_eq)
  also from sym [OF l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f "(\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)"]] and f_hom_diff and pert_in_R h_in_R phi_in_R
  have "\<dots> = f \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) \<circ> g" unfolding hom_diff_def by simp
  also from phi_prop have "\<dots> = f \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g" by simp
  also from minus_dist_comp [OF C_diff_group _ R.one_closed, of g "\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h"] and g_hom_diff and phi_in_R pert_in_R h_in_R
  have "\<dots> = f \<circ> (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x \<otimes> (\<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g) x else \<one>)" 
    by (unfold hom_diff_def, simp add: expand_fun_eq)
  also have "\<dots> = f \<circ> (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x else \<one>)"
  proof -
    have "(\<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g) = \<ominus>\<^bsub>R\<^esub> \<zero>\<^bsub>R\<^esub> \<circ> g" 
    proof -
      from hg and ring_R and hom_completion_one [of D D \<delta>] hom_completion_one [of D D \<Phi>] and D.diff_group_is_group and pert_in_R and phi_in_R
      have "(\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g = \<zero>\<^bsub>R\<^esub> \<circ> g" by (simp add: expand_fun_eq)
      with minus_comp_g2 [OF C_diff_group _ _ R.zero_closed, of g "\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h"] and g_hom_diff and phi_in_R pert_in_R h_in_R
      show "(\<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g) = \<ominus>\<^bsub>R\<^esub> \<zero>\<^bsub>R\<^esub> \<circ> g" unfolding hom_diff_def by simp
    qed
    also have "\<dots> = \<zero>\<^bsub>R\<^esub> \<circ> g" by simp
    also from ring_R have "\<dots> = (\<lambda>x. \<one>)" by (simp add: expand_fun_eq)
    finally have "\<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h) \<circ> g = (\<lambda>x. \<one>)" by simp
    with D.r_one and g_hom_diff and hom_completion_closed [of g C D] and ring_R show ?thesis by (simp add: expand_fun_eq)
  qed
  also from comp_hom_compl [OF C_diff_group _ R.one_closed, of g] and g_hom_diff have "\<dots> = f \<circ> (\<one>\<^bsub>R\<^esub> \<circ> g)" unfolding hom_diff_def by simp
  also from g_hom_diff and hom_completion_closed [of g C D] and ring_R have "\<dots> = f \<circ> g"
  proof -
    from g_hom_diff and hom_completion_closed [of g C D] and ring_R have "(\<one>\<^bsub>R\<^esub> \<circ> g) = g"
      unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
    then show ?thesis by simp
  qed
  also from fg have "\<dots> = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)" by simp
  finally show "f \<circ> \<pi>' \<circ> g = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)" by simp
qed

lemma (in BPL) \<pi>'g_eq_psig: shows "\<pi>' \<circ> g  = \<Psi> \<circ> g"
proof -
  from \<pi>'_def have "\<pi>' \<circ> g = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') \<circ> g" by simp
  also from minus_dist_comp [of C g "\<one>\<^bsub>R\<^esub>" p'] and p'_in_R and R.one_closed and g_hom_diff and C_diff_group
  have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x \<otimes> ((\<ominus>\<^bsub>R\<^esub> p') \<circ> g) x else \<one>)" by (unfold hom_diff_def, simp)
  also from psi_in_R h_in_R pert_in_R and minus_comp_g2 [OF C_diff_group, of g p' "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>"]  and p'g_eq_psihdeltag and g_hom_diff
  have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x \<otimes> (\<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g) x else \<one>)"
    unfolding hom_diff_def by (auto simp add: expand_fun_eq)
  also from sym [OF minus_dist_comp [OF C_diff_group _ R.one_closed, of g "(\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)"]] and g_hom_diff and pert_in_R h_in_R phi_in_R
  have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)) \<circ> g" unfolding hom_diff_def by simp
  also from psi_prop have "\<dots> = \<Psi> \<circ> g" by simp
  finally show ?thesis by simp
qed

subsection{*BPL simplification*}

text{*Now we can prove the simplifications of the terms in the reduction; these simplification processes correspond 
  to the ones in pages 56 and 57 of Aransay's memoir*}

lemma (in BPL) BPL_simplifications: shows f: "(f' \<circ> (\<tau>' \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')) = f \<circ> \<Phi>" and g: "(inc_ker_p' \<circ> \<tau> \<circ> g) = \<Psi> \<circ> g" 
  and diff_C: "f' \<circ> (\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<Psi> \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
proof -
  show "f' \<circ> (\<tau>' \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') = f \<circ> \<Phi>" 
    (*The proof is divided into 3 parts; first we prove f' \<circ> (\<tau>' \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') = f' \<circ> (\<pi> \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')*)
    (*Then we prove that f' \<circ> (\<pi> \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') = f \<circ> (\<pi> \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')*)
    (*Then we deal with this expression, proving that f \<circ> \<pi> = f, and finally, the hardest part, that f \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p' = f \<circ> \<Phi>*)
  proof -
    have "f' \<circ> (\<tau>' \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') = f' \<circ> (\<tau>' \<circ> \<pi>')" unfolding \<pi>'_def by simp
    also have "\<dots> = f' \<circ> (\<pi> \<circ> \<pi>')" unfolding \<tau>'\<pi>'_eq_\<pi>\<pi>' by simp
    also have "\<dots> = f \<circ> \<pi> \<circ> \<pi>'" unfolding o_assoc unfolding f'\<pi>_eq_f\<pi> by simp
    also have "\<dots> = f \<circ> \<pi>'" unfolding f\<pi>_eq_f by simp
    also have "\<dots> = f \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p')" unfolding \<pi>'_def by simp
    also from l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f p'] and p'_in_R and f_hom_diff and C_diff_group
    have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<one>\<^bsub>R\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> (\<ominus>\<^bsub>R\<^esub> p')) x else \<one>\<^bsub>C\<^esub>)" unfolding hom_diff_def by simp
    also from phi_in_R h_in_R pert_in_R and l_minus_comp_f [OF C_diff_group, of f p' "\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>"]  and fp'_eq_fdeltahphi and f_hom_diff
    have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> \<one>\<^bsub>R\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) x else \<one>\<^bsub>C\<^esub>)"
      unfolding hom_diff_def by (auto simp add: expand_fun_eq)
    also from sym [OF l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f "(\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)"]] and f_hom_diff and pert_in_R h_in_R phi_in_R
    have "\<dots> = f \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>))" unfolding hom_diff_def by simp
    also from phi_prop have "\<dots> = f \<circ> \<Phi>" by simp
    finally show ?thesis by simp
  qed
next
  show "(inc_ker_p' \<circ> \<tau> \<circ> g) = \<Psi> \<circ> g"
  proof -
    have "inc_ker_p' \<circ> \<tau> \<circ> g = \<tau> \<circ> g" unfolding inc_ker_p\<tau>_eq_\<tau> by simp
    also have "\<dots> = \<pi>' \<circ> g" unfolding \<tau>g_eq_\<pi>'g by simp
    (*This part of the proof corresponds exactly to lemma \<pi>'g_eq_psig; the reason for maintaining it here is for keeping the similarity 
      to the proof in the memoir*)
    also have "\<pi>' \<circ> g = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p') \<circ> g" unfolding \<pi>'_def by simp
    also from minus_dist_comp [of C g "\<one>\<^bsub>R\<^esub>" p'] and p'_in_R and R.one_closed and g_hom_diff and C_diff_group
    have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x \<otimes> ((\<ominus>\<^bsub>R\<^esub> p') \<circ> g) x else \<one>)" unfolding hom_diff_def by simp
    also from psi_in_R h_in_R pert_in_R and minus_comp_g2 [OF C_diff_group, of g p' "\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>"]  and p'g_eq_psihdeltag and g_hom_diff
    have "\<dots> = (\<lambda>x. if x \<in> carrier C then (\<one>\<^bsub>R\<^esub> \<circ> g) x \<otimes> (\<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>) \<circ> g) x else \<one>)"
      unfolding hom_diff_def by (auto simp add: expand_fun_eq)
    also from sym [OF minus_dist_comp [OF C_diff_group _ R.one_closed, of g "(\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)"]] and g_hom_diff and pert_in_R h_in_R phi_in_R
    have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)) \<circ> g" unfolding hom_diff_def by simp
    also from psi_prop have "\<dots> = \<Psi> \<circ> g" by simp
    finally show ?thesis by simp
  qed
next
  show "f' \<circ> (\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<Psi> \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
    (is "f' \<circ> (\<tau>' \<circ> ?diff_ker_p' \<circ> \<tau>) \<circ> g = ?diff_C_pert")
  proof -
    have "f' \<circ> (\<tau>' \<circ> ?diff_ker_p' \<circ> \<tau>) \<circ> g = (f' \<circ> \<tau>') \<circ> ?diff_ker_p' \<circ> (\<tau> \<circ> g)" by (simp add: o_assoc)
    also from \<tau>g_eq_\<pi>'g have "\<dots> = (f' \<circ> \<tau>') \<circ> ?diff_ker_p' \<circ> (\<pi>' \<circ> g)" by simp
    also have "\<dots> = f' \<circ> (\<tau>' \<circ> ?diff_ker_p') \<circ> \<pi>' \<circ> g" by (simp add: o_assoc)
    also from \<tau>'diff'_eq_\<pi>diff' have "\<dots> = f' \<circ> (\<pi> \<circ> differ\<^bsub>diff_group_ker_p'\<^esub>) \<circ> \<pi>' \<circ> g" by (simp add: expand_fun_eq)
    also have "\<dots> = f' \<circ> \<pi> \<circ> (differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<pi>') \<circ> g" by (simp add: o_assoc)
    also from diff_ker_p'\<pi>'_eq_diff'\<pi>' have "\<dots> = f' \<circ> \<pi> \<circ> (diff' \<circ> \<pi>') \<circ> g" by (simp add: expand_fun_eq)
    also from f'\<pi>_eq_f\<pi> have "\<dots> = f \<circ> \<pi> \<circ> (diff' \<circ> \<pi>') \<circ> g" by simp
    also from f\<pi>_eq_f have "\<dots> = f \<circ> (diff' \<circ> \<pi>') \<circ> g" by simp
    also have "\<dots> = f \<circ> diff' \<circ> (\<pi>' \<circ> g)" by (simp add: o_assoc)
    also from diff'_def have "\<dots> = f \<circ> (differ \<oplus>\<^bsub>R\<^esub> \<delta>) \<circ> (\<pi>' \<circ> g)" by simp
    also have "\<dots> = f \<circ> ((differ \<oplus>\<^bsub>R\<^esub> \<delta>) \<circ> \<pi>') \<circ> g" by (simp add: o_assoc)
    also from ring_R have "\<dots> = f \<circ> ((differ \<oplus>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<pi>') \<circ> g" by simp
    also from \<pi>'_in_R and diff_in_R and pert_in_R and R.one_closed have "\<dots> = f \<circ> (differ \<otimes>\<^bsub>R\<^esub> \<pi>' \<oplus>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<pi>') \<circ> g" by algebra
    also from l_add_dist_comp [OF C_diff_group, of f "differ \<otimes>\<^bsub>R\<^esub> \<pi>'" "\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>'"] f_hom_diff diff_in_R \<pi>'_in_R pert_in_R
    have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> (differ \<otimes>\<^bsub>R\<^esub> \<pi>')) x \<otimes>\<^bsub>C \<^esub> (f \<circ> (\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>')) x else \<one>\<^bsub>C\<^esub>) \<circ> g" by (unfold hom_diff_def, simp)
    also from ring_R and o_assoc have "\<dots> = (\<lambda>x. if x \<in> carrier D then (f \<circ> differ \<circ> \<pi>') x \<otimes>\<^bsub>C \<^esub> (f \<circ> (\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>')) x else \<one>\<^bsub>C\<^esub>) \<circ> g" 
      by (simp add: expand_fun_eq)
    also from hom_diff_coherent [OF f_hom_diff] 
    have "\<dots> =  (\<lambda>x. if x \<in> carrier D then (differ\<^bsub>C\<^esub> \<circ> f \<circ> \<pi>') x \<otimes>\<^bsub>C \<^esub> (f \<circ> (\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>')) x else \<one>\<^bsub>C\<^esub>) \<circ> g" by (simp add: expand_fun_eq)
    also have "\<dots> = (\<lambda>x. if x \<in> carrier C then ((differ\<^bsub>C\<^esub> \<circ> f \<circ> \<pi>') \<circ> g) x \<otimes>\<^bsub>C \<^esub> ((f \<circ> (\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>')) \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
    proof (auto simp add: expand_fun_eq)
      fix x
      assume x: "x \<in> carrier C" and "g x \<notin> carrier D" with g_hom_diff and hom_completion_closed [of g C D] 
      show "\<one>\<^bsub>C\<^esub> = (differ\<^bsub>C\<^esub>) (f (\<pi>' (g x))) \<otimes>\<^bsub>C\<^esub> f ((\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>') (g x))" by (unfold hom_diff_def, simp)
    next
      fix x
      assume "x \<notin> carrier C" with completion_closed2 [of g C D x] and g_hom_diff have g_x: "g x = \<one>"
	by (unfold hom_diff_def hom_completion_def, simp)
      with hom_completion_one [of D D \<pi>'] and \<pi>'_in_R and ring_R and D.diff_group_is_group
	and hom_completion_one [of D C f] and C.diff_group_is_group and f_hom_diff
	and hom_completion_one [of C C "differ\<^bsub>C\<^esub>"] and diff_group.diff_hom [OF C_diff_group]
	and hom_completion_one [of D D "\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>'"] and pert_in_R and R.m_closed [of \<delta> \<pi>']
      show " (differ\<^bsub>C\<^esub>) (f (\<pi>' (g x))) \<otimes>\<^bsub>C\<^esub> f ((\<delta> \<otimes>\<^bsub>R\<^esub> \<pi>') (g x)) = \<one>\<^bsub>C\<^esub>" by (unfold hom_diff_def, auto)
    qed
    also from ring_R have "\<dots> = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub> \<circ> (f \<circ> \<pi>' \<circ> g)) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<pi>' \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
      by (simp add: o_assoc expand_fun_eq)
    also from f\<pi>'g_eq_id and diff_group.diff_hom [OF C_diff_group] 
    have "\<dots> = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<pi>' \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
      by (unfold hom_completion_def completion_fun2_def completion_def, auto simp add: expand_fun_eq)
    also from \<pi>'g_eq_psig have "\<dots> = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<Psi> \<circ> g) x else \<one>\<^bsub>C\<^esub>)" by (simp add: expand_fun_eq)
    finally show " f' \<circ> (\<tau>' \<circ> differ\<^bsub>diff_group_ker_p'\<^esub> \<circ> \<tau>) \<circ> g = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<Psi> \<circ> g) x else \<one>\<^bsub>C\<^esub>)"
      by simp
  qed
qed

text{*By joining @{thm [locale=BPL] BPL_reduction} and @{thm [locale=BPL] BPL_simplifications} we get the proof of the BPL, 
  stated as in @{text "Lemma 2.2.20"} in Aransay's memoir*}

lemma (in BPL) BPL: shows "reduction D' 
  \<lparr> carrier = carrier C, mult = mult C, one = one C, diff = (\<lambda>x. if x \<in> carrier C then (differ\<^bsub>C\<^esub>) x \<otimes>\<^bsub>C\<^esub> (f \<circ> \<delta> \<circ> \<Psi> \<circ> g) x else \<one>\<^bsub>C\<^esub>)\<rparr> 
  (f \<circ> \<Phi>) (\<Psi> \<circ> g) h'"
using BPL_reduction and BPL_simplifications by simp

end