# Theory QuasiBorel

```(*  Title:   QuasiBorel.thy
Author:  Yasuhiko Minamide, Michikazu Hirata, Tokyo Institute of Technology
*)

section ‹Quasi-Borel Spaces›
theory QuasiBorel
imports "StandardBorel"
begin

subsection ‹ Definitions ›

text ‹ We formalize quasi-Borel spaces introduced by Heunen et al.~\<^cite>‹"Heunen_2017"›.›

subsubsection ‹ Quasi-Borel Spaces›
definition qbs_closed1 :: "(real ⇒ 'a) set ⇒ bool"
where "qbs_closed1 Mx ≡ (∀a ∈ Mx. ∀f ∈ real_borel →⇩M real_borel. a ∘ f ∈ Mx)"

definition qbs_closed2 :: "['a set, (real ⇒ 'a) set] ⇒ bool"
where "qbs_closed2 X Mx ≡ (∀x ∈ X. (λr. x) ∈ Mx)"

definition qbs_closed3 :: "(real ⇒ 'a) set ⇒ bool"
where "qbs_closed3 Mx ≡ (∀P::real ⇒ nat. ∀Fi::nat ⇒ real ⇒ 'a.
(∀i. P -` {i} ∈ sets real_borel)
⟶ (∀i. Fi i ∈ Mx)
⟶ (λr. Fi (P r) r) ∈ Mx)"

lemma separate_measurable:
fixes P :: "real ⇒ nat"
assumes "⋀i. P -` {i} ∈ sets real_borel"
shows "P ∈ real_borel →⇩M nat_borel"
proof -
have "P ∈ real_borel →⇩M count_space UNIV"
by (auto simp add: assms measurable_count_space_eq_countable)
thus ?thesis
using measurable_cong_sets sets_borel_eq_count_space by blast
qed

lemma measurable_separate:
fixes P :: "real ⇒ nat"
assumes "P ∈ real_borel →⇩M nat_borel"
shows "P -` {i} ∈ sets real_borel"
by(rule measurable_sets_borel[OF assms borel_singleton[OF sets.empty_sets,of i]])

definition "is_quasi_borel X Mx ⟷ Mx ⊆ UNIV → X ∧ qbs_closed1 Mx ∧ qbs_closed2 X Mx ∧ qbs_closed3 Mx"

lemma is_quasi_borel_intro[simp]:
assumes "Mx ⊆ UNIV → X"
and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx"
shows "is_quasi_borel X Mx"

typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}"
proof
show "(UNIV, UNIV) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
qed

definition qbs_space :: "'a quasi_borel ⇒ 'a set" where
"qbs_space X ≡ fst (Rep_quasi_borel X)"

definition qbs_Mx :: "'a quasi_borel ⇒ (real ⇒ 'a) set" where
"qbs_Mx X ≡ snd (Rep_quasi_borel X)"

lemma qbs_decomp :
"(qbs_space X,qbs_Mx X) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified])

lemma qbs_Mx_to_X[dest]:
assumes "α ∈ qbs_Mx X"
shows "α ∈ UNIV → qbs_space X"
"α r ∈ qbs_space X"
using qbs_decomp assms by(auto simp: is_quasi_borel_def)

lemma qbs_closed1I:
assumes "⋀α f. α ∈ Mx ⟹ f ∈ real_borel →⇩M real_borel ⟹ α ∘ f ∈ Mx"
shows "qbs_closed1 Mx"

lemma qbs_closed1_dest[simp]:
assumes "α ∈ qbs_Mx X"
and "f ∈ real_borel →⇩M real_borel"
shows "α ∘ f ∈ qbs_Mx X"
using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def)

lemma qbs_closed2I:
assumes "⋀x. x ∈ X ⟹ (λr. x) ∈ Mx"
shows "qbs_closed2 X Mx"

lemma qbs_closed2_dest[simp]:
assumes "x ∈ qbs_space X"
shows "(λr. x) ∈ qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def)

lemma qbs_closed3I:
assumes "⋀(P :: real ⇒ nat) Fi. (⋀i. P -` {i} ∈ sets real_borel) ⟹ (⋀i. Fi i ∈ Mx)
⟹ (λr. Fi (P r) r) ∈ Mx"
shows "qbs_closed3 Mx"
using assms by(auto simp: qbs_closed3_def)

lemma qbs_closed3I':
assumes "⋀(P :: real ⇒ nat) Fi. P ∈ real_borel →⇩M nat_borel ⟹ (⋀i. Fi i ∈ Mx)
⟹ (λr. Fi (P r) r) ∈ Mx"
shows "qbs_closed3 Mx"
using assms by(auto intro!: qbs_closed3I simp: separate_measurable)

lemma qbs_closed3_dest[simp]:
fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
assumes "⋀i. P -` {i} ∈ sets real_borel"
and "⋀i. Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def)

lemma qbs_closed3_dest':
fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
assumes "P ∈ real_borel →⇩M nat_borel"
and "⋀i. Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
using qbs_closed3_dest[OF measurable_separate[OF assms(1)] assms(2)] .

lemma qbs_closed3_dest2:
assumes "countable I"
and [measurable]: "P ∈ real_borel →⇩M count_space I"
and "⋀i. i ∈ I ⟹ Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
have 0:"I ≠ {}"
using measurable_empty_iff[of "count_space I" P real_borel] assms(2)
by fastforce
define P' where "P' ≡ to_nat_on I ∘ P"
define Fi' where "Fi' ≡ Fi ∘ (from_nat_into I)"
have 1:"P' ∈ real_borel →⇩M nat_borel"
have 2:"⋀i. Fi' i ∈ qbs_Mx X"
using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def)
have "(λr. Fi' (P' r) r) ∈ qbs_Mx X"
using 1 2 measurable_separate by auto
thus ?thesis
using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)]
by(auto simp: Fi'_def P'_def)
qed

lemma qbs_closed3_dest2':
assumes "countable I"
and [measurable]: "P ∈ real_borel →⇩M count_space I"
and "⋀i. i ∈ range P ⟹ Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
have 0:"range P ∩ I = range P"
using measurable_space[OF assms(2)] by auto
have 1:"P ∈ real_borel →⇩M count_space (range P)"
using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"]
have 2:"countable (range P)"
using countable_Int2[OF assms(1),of "range P"]
show ?thesis
by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)])
qed

lemma qbs_space_Mx:
"qbs_space X = {α x |x α. α ∈ qbs_Mx X}"
proof auto
fix x
assume 1:"x ∈ qbs_space X"
show "∃xa α. x = α xa ∧ α ∈ qbs_Mx X"
by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1)
qed

lemma qbs_space_eq_Mx:
assumes "qbs_Mx X = qbs_Mx Y"
shows "qbs_space X = qbs_space Y"

lemma qbs_eqI:
assumes "qbs_Mx X = qbs_Mx Y"
shows "X = Y"
by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms])

subsubsection ‹ Morphism of Quasi-Borel Spaces ›
definition qbs_morphism :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a ⇒ 'b) set" (infixr "→⇩Q" 60) where
"X →⇩Q Y ≡ {f ∈ qbs_space X → qbs_space Y. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"

lemma qbs_morphismI:
assumes "⋀α. α ∈ qbs_Mx X ⟹ f ∘ α ∈ qbs_Mx Y"
shows "f ∈ X →⇩Q Y"
proof -
have "f ∈ qbs_space X → qbs_space Y"
proof
fix x
assume "x ∈ qbs_space X "
then have "(λr. x) ∈ qbs_Mx X"
by simp
hence "f ∘ (λr. x) ∈ qbs_Mx Y"
using assms by blast
thus "f x ∈ qbs_space Y"
by auto
qed
thus ?thesis
qed

lemma qbs_morphismE[dest]:
assumes "f ∈ X →⇩Q Y"
shows "f ∈ qbs_space X → qbs_space Y"
"⋀x. x ∈ qbs_space X ⟹ f x ∈ qbs_space Y"
"⋀α. α ∈ qbs_Mx X ⟹ f ∘ α ∈ qbs_Mx Y"
using assms by(auto simp add: qbs_morphism_def)

lemma qbs_morphism_ident[simp]:
"id ∈ X →⇩Q X"
by(auto intro: qbs_morphismI)

lemma qbs_morphism_ident'[simp]:
"(λx. x) ∈ X →⇩Q X"

lemma qbs_morphism_comp:
assumes "f ∈ X →⇩Q Y" "g ∈ Y →⇩Q Z"
shows "g ∘ f ∈ X →⇩Q Z"
using assms by (simp add: comp_assoc Pi_def qbs_morphism_def)

lemma qbs_morphism_cong:
assumes "⋀x. x ∈ qbs_space X ⟹ f x = g x"
and "f ∈ X →⇩Q Y"
shows "g ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume 1:"α ∈ qbs_Mx X"
have "g ∘ α = f ∘ α"
proof
fix x
have "α x ∈ qbs_space X"
using 1 qbs_decomp[of X] by auto
thus "(g ∘ α) x = (f ∘ α) x"
using assms(1) by simp
qed
thus "g ∘ α ∈ qbs_Mx Y"
using 1 assms(2) by(simp add: qbs_morphism_def)
qed

lemma qbs_morphism_const:
assumes "y ∈ qbs_space Y"
shows "(λ_. y) ∈ X →⇩Q Y"
using assms by (auto intro: qbs_morphismI)

subsubsection ‹ Empty Space ›
definition empty_quasi_borel  :: "'a quasi_borel" where
"empty_quasi_borel ≡ Abs_quasi_borel ({},{})"

lemma eqb_correct: "Rep_quasi_borel empty_quasi_borel = ({}, {})"
using Abs_quasi_borel_inverse
by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma eqb_space[simp]: "qbs_space empty_quasi_borel = {}"

lemma eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = {}"

lemma qbs_empty_equiv :"qbs_space X = {} ⟷ qbs_Mx X = {}"
proof(auto)
fix x
assume "qbs_Mx X = {}"
and h:"x ∈ qbs_space X"
have "(λr. x) ∈ qbs_Mx X"
using h by simp
thus "False" using ‹qbs_Mx X = {}› by simp
qed

lemma empty_quasi_borel_iff:
"qbs_space X = {} ⟷ X = empty_quasi_borel"
by(auto intro!: qbs_eqI)

subsubsection ‹ Unit Space ›
definition unit_quasi_borel :: "unit quasi_borel" ("1⇩Q") where
"unit_quasi_borel ≡ Abs_quasi_borel (UNIV,UNIV)"

lemma uqb_correct: "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)"
using Abs_quasi_borel_inverse
by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma uqb_space[simp]: "qbs_space unit_quasi_borel = {()}"

lemma uqb_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}"

lemma unit_quasi_borel_terminal:
"∃! f. f ∈ X →⇩Q unit_quasi_borel"
by(fastforce simp: qbs_morphism_def)

definition to_unit_quasi_borel :: "'a ⇒ unit" ("!⇩Q") where
"to_unit_quasi_borel ≡ (λ_.())"

lemma to_unit_quasi_borel_morphism :
"!⇩Q ∈ X →⇩Q unit_quasi_borel"

subsubsection ‹ Subspaces ›
definition sub_qbs :: "['a quasi_borel, 'a set] ⇒ 'a quasi_borel" where
"sub_qbs X U ≡ Abs_quasi_borel (qbs_space X ∩ U,{f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X})"

lemma sub_qbs_closed:
"qbs_closed1 {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
"qbs_closed2 (qbs_space X ∩ U) {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
"qbs_closed3 {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto

lemma sub_qbs_correct[simp]: "Rep_quasi_borel (sub_qbs X U) = (qbs_space X ∩ U,{f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X})"

lemma sub_qbs_space[simp]: "qbs_space (sub_qbs X U) = qbs_space X ∩ U"

lemma sub_qbs_Mx[simp]: "qbs_Mx (sub_qbs X U) = {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"

lemma sub_qbs:
assumes "U ⊆ qbs_space X"
shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f ∈ UNIV → U. f ∈ qbs_Mx X})"
using assms by auto

subsubsection ‹ Image Spaces ›
definition map_qbs :: "['a ⇒ 'b] ⇒ 'a quasi_borel ⇒ 'b quasi_borel" where
"map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{β. ∃α∈ qbs_Mx X. β = f ∘ α})"

lemma map_qbs_f:
"{β. ∃α∈ qbs_Mx X. β = f ∘ α} ⊆ UNIV → f ` (qbs_space X)"
by fastforce

lemma map_qbs_closed1:
"qbs_closed1 {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
unfolding qbs_closed1_def
using qbs_closed1_dest by(fastforce simp: comp_def)

lemma map_qbs_closed2:
"qbs_closed2 (f ` (qbs_space X)) {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
unfolding qbs_closed2_def by fastforce

lemma map_qbs_closed3:
"qbs_closed3 {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
fix P Fi
assume h:"∀i::nat. P -` {i} ∈ sets real_borel"
"∀i::nat. ∃α∈qbs_Mx X. Fi i = f ∘ α"
then obtain αi
where ha: "∀i::nat. αi i ∈ qbs_Mx X ∧  Fi i = f ∘ (αi i)"
by metis
hence 1:"(λr. αi (P r) r) ∈ qbs_Mx X"
using h(1) by fastforce
show "∃α∈qbs_Mx X. (λr. Fi (P r) r) = f ∘ α"
by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def)
qed

lemma map_qbs_correct[simp]:
"Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{β. ∃α∈ qbs_Mx X. β = f ∘ α})"
unfolding map_qbs_def
by(simp add: Abs_quasi_borel_inverse map_qbs_f map_qbs_closed1 map_qbs_closed2 map_qbs_closed3)

lemma map_qbs_space[simp]:
"qbs_space (map_qbs f X) = f ` (qbs_space X)"

lemma map_qbs_Mx[simp]:
"qbs_Mx (map_qbs f X) = {β. ∃α∈ qbs_Mx X. β = f ∘ α}"

inductive_set generating_Mx :: "'a set ⇒ (real ⇒ 'a) set ⇒ (real ⇒ 'a) set"
for X :: "'a set" and Mx :: "(real ⇒ 'a) set"
where
Basic: "α ∈ Mx ⟹ α ∈ generating_Mx X Mx"
| Const: "x ∈ X ⟹ (λr. x) ∈ generating_Mx X Mx"
| Comp : "f ∈ real_borel →⇩M real_borel ⟹ α ∈ generating_Mx X Mx ⟹ α ∘ f ∈ generating_Mx X Mx"
| Part : "(⋀i. Fi i ∈ generating_Mx X Mx) ⟹ P ∈ real_borel →⇩M nat_borel ⟹ (λr. Fi (P r) r) ∈ generating_Mx X Mx"

lemma generating_Mx_to_space:
assumes "Mx ⊆ UNIV → X"
shows "generating_Mx X Mx ⊆ UNIV → X"
proof
fix α
assume "α ∈ generating_Mx X Mx"
then show "α ∈ UNIV → X"
by(induct rule: generating_Mx.induct) (use assms in auto)
qed

lemma generating_Mx_closed1:
"qbs_closed1 (generating_Mx X Mx)"

lemma generating_Mx_closed2:
"qbs_closed2 X (generating_Mx X Mx)"

lemma generating_Mx_closed3:
"qbs_closed3 (generating_Mx X Mx)"

lemma generating_Mx_Mx:
"generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X"
proof auto
fix α
assume "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)"
then show "α ∈ qbs_Mx X"
by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest')
next
fix α
assume "α ∈ qbs_Mx X"
then show "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)" ..
qed

subsubsection ‹ Ordering of Quasi-Borel Spaces ›

instantiation quasi_borel :: (type) order_bot
begin

inductive less_eq_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
"qbs_space X ⊂ qbs_space Y ⟹ less_eq_quasi_borel X Y"
| "qbs_space X = qbs_space Y ⟹ qbs_Mx Y ⊆ qbs_Mx X ⟹ less_eq_quasi_borel X Y"

lemma le_quasi_borel_iff:
"X ≤ Y ⟷ (if qbs_space X = qbs_space Y then qbs_Mx Y ⊆ qbs_Mx X else qbs_space X ⊂ qbs_space Y)"
by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros)

definition less_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
"less_quasi_borel X Y ⟷ (X ≤ Y ∧ ¬ Y ≤ X)"

definition bot_quasi_borel :: "'a quasi_borel" where
"bot_quasi_borel = empty_quasi_borel"

instance
proof
show "bot ≤ a" for a :: "'a quasi_borel"
using qbs_empty_equiv
qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI)
end

definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel] ⇒ 'a quasi_borel" where
"inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"

lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"
by(fastforce intro!: Abs_quasi_borel_inverse
simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)

lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X ∩ qbs_space X'"

lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X ∩ qbs_Mx X'"

definition max_quasi_borel :: "'a set ⇒ 'a quasi_borel" where
"max_quasi_borel X = Abs_quasi_borel (X, UNIV → X)"

lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV → X)"
by(fastforce intro!: Abs_quasi_borel_inverse
simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X"

lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV → X"

instantiation quasi_borel :: (type) semilattice_sup
begin

definition sup_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ 'a quasi_borel" where
"sup_quasi_borel X Y ≡ (if qbs_space X = qbs_space Y      then inf_quasi_borel X Y
else if qbs_space X ⊂ qbs_space Y then Y
else if qbs_space Y ⊂ qbs_space X then X
else max_quasi_borel (qbs_space X ∪ qbs_space Y))"

instance
proof
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "X ≤ X ⊔ Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "Y ≤ X ⊔ Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y Z :: "'a quasi_borel"
assume h:"X ≤ Z" "Y ≤ Z"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
let ?Z = "qbs_space Z"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "sup X Y ≤ Z"
proof cases
case 1
show ?thesis
unfolding sup_quasi_borel_def
apply(rule less_eq_quasi_borel.intros(1))
apply auto[1]
apply auto
apply(rule less_eq_quasi_borel.intros(2))
by(rule less_eq_quasi_borel.cases[OF h(2)]) (auto simp: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
using h(2) by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
using h(1) by auto
next
case 4
then have [simp]:"?X ≠ ?Y" "~ (?X ⊂ ?Y)" "~ (?Y ⊂ ?X)"
by auto
have [simp]:"?X ⊆ ?Z" "?Y ⊆ ?Z"
by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases)
(metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases)
then consider "?X ∪ ?Y = ?Z" | "?X ∪ ?Y ⊂ ?Z"
by blast
then show ?thesis
unfolding sup_quasi_borel_def
apply cases
apply simp
apply(rule less_eq_quasi_borel.intros(2))
apply simp
apply auto[1]