Theory Transport_Functions_Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Relator›
theory Transport_Functions_Galois_Relator
  imports
    Transport_Functions_Relation_Simplifications
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

interpretation flip : transport_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.t1.counit ≡ η⇩1" by (simp only: t1.flip_counit_eq_unit)

lemma Dep_Fun_Rel_left_Galois_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_r2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and L2_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and ge_L2_r2_le2: "⋀x x' y'. x ⇘L1⇙⪅ x' ⟹ in_dom (≤⇘R2 (l1 x) x'⇙) y' ⟹
    (≥⇘L2 x (r1 x')⇙) (r2⇘x (l1 x)⇙ y') ≤ (≥⇘L2 x (r1 x')⇙) (r2⇘x x'⇙ y')"
  and trans_L2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  and "f ⇘L⇙⪅ g"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
proof (intro Dep_Fun_Rel_relI)
  fix x x' assume "x ⇘L1⇙⪅ x'"
  show "f x ⇘L2 x x'⇙⪅ g x'"
  proof (intro t2.left_GaloisI)
    from ‹x ⇘L1⇙⪅ x'› ‹((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1› have "x ≤⇘L1⇙ r1 x'" "l1 x ≤⇘R1⇙ x'" by auto
    with ‹g ≤⇘R⇙ g› have "g (l1 x) ≤⇘R2 (l1 x) x'⇙ g x'" by blast
    then show "in_codom (≤⇘R2 (l1 x) x'⇙) (g x')" by blast

    from ‹f ⇘L⇙⪅ g› have "f ≤⇘L⇙ r g" by blast
    moreover from refl_L1 ‹x ⇘L1⇙⪅ x'› have "x ≤⇘L1⇙ x" by blast
    ultimately have "f x ≤⇘L2 x x⇙ (r g) x" by blast
    with L2_le2 ‹x ≤⇘L1⇙ r1 x'› have "f x ≤⇘L2 x (r1 x')⇙ (r g) x" by blast
    then have "f x ≤⇘L2 x (r1 x')⇙ r2⇘x (l1 x)⇙ (g (l1 x))" by simp
    with ge_L2_r2_le2 have "f x ≤⇘L2 x (r1 x')⇙ r2⇘x x'⇙ (g (l1 x))"
      using ‹x ⇘L1⇙⪅ x'› ‹g (l1 x) ≤⇘R2 (l1 x) x'⇙ _› by blast
    moreover have "... ≤⇘L2 x (r1 x')⇙ r2⇘x x'⇙ (g x')"
      using mono_r2 ‹x ⇘L1⇙⪅ x'› ‹g (l1 x) ≤⇘R2 (l1 x) x'⇙ g x'› by blast
    ultimately show "f x ≤⇘L2 x (r1 x')⇙ r2⇘x x'⇙ (g x')"
      using trans_L2 ‹x ⇘L1⇙⪅ x'› by blast
  qed
qed

lemma left_rel_right_if_Dep_Fun_Rel_left_GaloisI:
  assumes mono_l1: "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and half_galois_prop_right1: "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and L2_unit_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and ge_L2_r2_le1: "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and rel_f_g: "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  shows "f ≤⇘L⇙ r g"
proof (intro left_relI)
  fix x1 x2 assume "x1 ≤⇘L1⇙ x2"
  with mono_l1 half_galois_prop_right1 have "x1 ⇘L1⇙⪅ l1 x2"
    by (intro t1.left_Galois_left_if_left_relI) auto
  with rel_f_g have "f x1 ⇘L2 x1 (l1 x2)⇙⪅ g (l1 x2)" by blast
  then have "in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) (g (l1 x2))"
    "f x1 ≤⇘L2 x1 (η⇩1 x2)⇙ r2⇘x1 (l1 x2)⇙ (g (l1 x2))" by auto
  with L2_unit_le2 ‹x1 ≤⇘L1⇙ x2› have "f x1 ≤⇘L2 x1 x2⇙ r2⇘x1 (l1 x2)⇙ (g (l1 x2))" by blast
  with ge_L2_r2_le1 ‹x1 ≤⇘L1⇙ x2› ‹in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) (g (l1 x2))›
    have "f x1 ≤⇘L2 x1 x2⇙ r2⇘x2 (l1 x2)⇙ (g (l1 x2))" by blast
  then show "f x1 ≤⇘L2 x1 x2⇙ r g x2" by simp
qed

lemma left_Galois_if_Dep_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and "in_codom (≤⇘R⇙) g"
  and "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  using assms by (intro left_GaloisI left_rel_right_if_Dep_Fun_Rel_left_GaloisI) auto

lemma left_right_rel_if_Dep_Fun_Rel_left_GaloisI:
  assumes mono_r1: "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and half_galois_prop_left2: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and R2_le1: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and R2_l2_le1: "⋀x1' x2' y. x1' ≤⇘R1⇙ x2' ⟹ in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) y ⟹
    (≤⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≤⇘R2 x1' x2'⇙) (l2⇘x1' (r1 x1')⇙ y)"
  and rel_f_g: "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  shows "l f ≤⇘R⇙ g"
proof (rule flip.left_relI)
  fix x1' x2' assume "x1' ≤⇘R1⇙ x2'"
  with mono_r1 have "r1 x1' ⇘L1⇙⪅ x2'" by blast
  with rel_f_g have "f (r1 x1') ⇘L2 (r1 x1') x2'⇙⪅ g x2'" by blast
  with half_galois_prop_left2[OF ‹x1' ≤⇘R1⇙ x2'›]
    have "l2⇘x2' (r1 x1')⇙ (f (r1 x1')) ≤⇘R2 (ε⇩1 x1') x2'⇙ g x2'" by auto
  with R2_le1 ‹x1' ≤⇘R1⇙ x2'› have "l2⇘x2' (r1 x1')⇙ (f (r1 x1')) ≤⇘R2 x1' x2'⇙ g x2'"
    by blast
  with R2_l2_le1 ‹x1' ≤⇘R1⇙ x2'› ‹f (r1 x1') ⇘L2 (r1 x1') x2'⇙⪅ _›
    have "l2⇘x1' (r1 x1')⇙ (f (r1 x1')) ≤⇘R2 x1' x2'⇙ g x2'" by blast
  then show "l f x1' ≤⇘R2 x1' x2'⇙ g x2'" by simp
qed

lemma left_Galois_if_Dep_Fun_Rel_left_GaloisI':
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and "⋀x1' x2' y. x1' ≤⇘R1⇙ x2' ⟹ in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) y ⟹
    (≤⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≤⇘R2 x1' x2'⇙) (l2⇘x1' (r1 x1')⇙ y)"
  and "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  using assms by (intro left_Galois_if_Dep_Fun_Rel_left_GaloisI in_codomI[where ?x="l f"])
  (auto intro!: left_right_rel_if_Dep_Fun_Rel_left_GaloisI)

lemma left_Galois_iff_Dep_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and "⋀x x' y'. x ⇘L1⇙⪅ x' ⟹ in_dom (≤⇘R2 (l1 x) x'⇙) y' ⟹
    (≥⇘L2 x (r1 x')⇙) (r2⇘x (l1 x)⇙ y') ≤ (≥⇘L2 x (r1 x')⇙) (r2⇘x x'⇙ y')"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro iffI)
  (auto intro!: Dep_Fun_Rel_left_Galois_if_left_GaloisI left_Galois_if_Dep_Fun_Rel_left_GaloisI)

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI:
  assumes "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹
    ((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  using assms by blast

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI':
  assumes "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((in_dom (≤⇘R2 (l1 x) x'⇙)) ⇛ (≤⇘L2 x (r1 x')⇙)) (r2⇘x (l1 x)⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "⋀x x' y'. x ⇘L1⇙⪅ x' ⟹ in_dom (≤⇘R2 (l1 x) x'⇙) y' ⟹
    (≥⇘L2 x (r1 x')⇙) (r2⇘x (l1 x)⇙ y') ≤ (≥⇘L2 x (r1 x')⇙) (r2⇘x x'⇙ y')"
  using assms by blast

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_codom_rightI:
  assumes mono_l1: "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and half_galois_prop_right1: "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and L2_le_unit2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "x1 ≤⇘L1⇙ x2"
  shows "((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
proof (intro Fun_Rel_predI)
  from mono_l1 half_galois_prop_right1 refl_L1 ‹x1 ≤⇘L1⇙ x2›
  have "l1 x2 ≤⇘R1⇙ l1 x2" "x2 ⇘L1⇙⪅ l1 x2"
    by (blast intro: t1.left_Galois_left_if_left_relI)+
  fix y' assume "in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y'"
  with Dep_Fun_Rel_relD[OF
    dep_mono_wrt_relD[OF mono_r2 ‹x1 ≤⇘L1⇙ x2›] ‹l1 x2 ≤⇘R1⇙ l1 x2›]
    have "r2⇘x1 (l1 x2)⇙ y' ≤⇘L2 x1 (η⇩1 x2)⇙ r2⇘x2 (l1 x2)⇙ y'"
    using ‹x2 ⇘L1⇙⪅ l1 x2› by (auto dest: in_field_if_in_codom)
  with L2_le_unit2 ‹x1 ≤⇘L1⇙ x2› show "r2⇘x1 (l1 x2)⇙ y' ≤⇘L2 x1 x2⇙ r2⇘x2 (l1 x2)⇙ y'"
    by blast
qed

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_dom_rightI:
  assumes mono_l1: "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and half_galois_prop_right1: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "x ⇘L1⇙⪅ x'"
  shows "((in_dom (≤⇘R2 (l1 x) x'⇙)) ⇛ (≤⇘L2 x (r1 x')⇙)) (r2⇘x (l1 x)⇙) (r2⇘x x'⇙)"
proof -
  from mono_l1 half_galois_prop_right1 refl_L1 ‹x ⇘L1⇙⪅ x'›
    have "x ≤⇘L1⇙ x" "l1 x ≤⇘R1⇙ x'" "x ⇘L1⇙⪅ l1 x"
    by (auto intro!: t1.half_galois_prop_leftD t1.left_Galois_left_if_left_relI)
  with Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹x ≤⇘L1⇙ x›] ‹l1 x ≤⇘R1⇙ x'›]
    show ?thesis by blast
qed

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_if_monoI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_GaloisI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI'
    left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_dom_rightI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_codom_rightI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom
    in_field_if_in_codom)

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_le_assmI:
  assumes refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_L2: "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "x1 ≤⇘L1⇙ x2"
  shows "(≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
proof -
  from refl_L1 ‹x1 ≤⇘L1⇙ x2› have "x1 ≤⇘L1⇙ x1" by blast
  with dep_mono_wrt_relD[OF dep_mono_wrt_predD[OF mono_L2] ‹x1 ≤⇘L1⇙ x2›]
    show "(≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)" by auto
qed

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assmI:
  assumes mono_l1: "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and half_galois_prop_right1: "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and antimono_L2:
    "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | (x1 ≤⇘L1⇙ x2 ∧ x3 ≤⇘L1⇙ η⇩1 x2)) ⇛⇩m (≥)) L2"
  and "x1 ≤⇘L1⇙ x2"
  shows "(≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
proof -
  from mono_l1 half_galois_prop_right1 refl_L1 ‹x1 ≤⇘L1⇙ x2› have "x2 ≤⇘L1⇙ η⇩1 x2"
    by (blast intro: t1.rel_unit_if_reflexive_on_if_half_galois_prop_right_if_mono_wrt_rel)
  with refl_L1 have "η⇩1 x2 ≤⇘L1⇙ η⇩1 x2" by blast
  with dep_mono_wrt_relD[OF dep_mono_wrt_predD[OF antimono_L2] ‹x2 ≤⇘L1⇙ η⇩1 x2›]
    show "(≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)" using ‹x1 ≤⇘L1⇙ x2› by auto
qed

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_if_monoI':
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | (x1 ≤⇘L1⇙ x2 ∧ x3 ≤⇘L1⇙ η⇩1 x2)) ⇛⇩m (≥)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_monoI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assmI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_le_assmI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom
    in_field_if_in_dom)

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | (x1 ≤⇘L1⇙ x2 ∧ x3 ≤⇘L1⇙ η⇩1 x2)) ⇛⇩m (≥)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_monoI') auto

interpretation flip_inv : galois "(≥⇘R1⇙)" "(≥⇘L1⇙)" r1 l1 .

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assm_if_galois_equivI:
  assumes galois_equiv1: "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_L2: "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "x1 ≤⇘L1⇙ x2"
  shows "(≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
proof -
  from refl_L1 ‹x1 ≤⇘L1⇙ x2› have "x1 ≤⇘L1⇙ x1" by blast
  from galois_equiv1 refl_L1 ‹x1 ≤⇘L1⇙ x2› have "η⇩1 x2 ≤⇘L1⇙ x2" by (intro
    flip.t1.counit_rel_if_reflexive_on_if_half_galois_prop_left_if_mono_wrt_rel)
    blast+
  have "x1 ≤⇘L1⇙ η⇩1 x2" by (rule t1.rel_unit_if_left_rel_if_mono_wrt_relI)
    (insert galois_equiv1 refl_L1 ‹x1 ≤⇘L1⇙ x2›, auto)
  with dep_mono_wrt_relD[OF dep_mono_wrt_predD[OF mono_L2] ‹η⇩1 x2 ≤⇘L1⇙ x2›]
    show "(≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)" by auto
qed

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro
    left_Galois_iff_Dep_Fun_Rel_left_Galois_if_monoI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_le_assmI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assm_if_galois_equivI)
  auto

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI
    reflexive_on_in_field_mono_assm_left2I)
  auto

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI')
  auto


corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI
    transitive_left2_if_preorder_equivalenceI)
  (auto 5 0)


subparagraph ‹Simplification of Restricted Function Relator›

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2' y. x1' ≤⇘R1⇙ x2' ⟹ in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) y ⟹
    (≤⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≤⇘R2 x1' x2'⇙) (l2⇘x1' (r1 x1')⇙ y)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙
    = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    in_domI[where ?y="r _"] left_rel_right_if_Dep_Fun_Rel_left_GaloisI
    in_codomI[where ?x="l _"] left_right_rel_if_Dep_Fun_Rel_left_GaloisI)
  auto

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇛⇩m (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙
    = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
  using assms by (intro
    Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI
    left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    reflexive_on_in_field_mono_assm_left2I
    left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI
    mono_wrt_rel_left_in_dom_mono_left_assm
    galois_connection_left_right_if_galois_connection_mono_assms_leftI
    galois_connection_left_right_if_galois_connection_mono_assms_rightI
    left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI)
  auto

text ‹Simplification of Restricted Function Relator for Nested Transports›

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq:
  fixes S :: "'a1 ⇒ 'a2 ⇒ 'b1 ⇒ 'b2 ⇒ bool"
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (S x x')↾⇘in_dom (≤⇘L2 x (r1 x')⇙)⇙↿⇘in_codom (≤⇘R2 (l1 x) x'⇙)⇙)
      ↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ =
    ((x x' ∷ (⇘L1⇙⪅)) ⇛ S x x')↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙" (is "?lhs = ?rhs")
proof -
  have "?lhs =
    ((x x' ∷ (⇘L1⇙⪅)) ⇛ (S x x')↿⇘in_codom (≤⇘R2 (l1 x) x'⇙)⇙)
      ↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
    by (subst rel_restrict_left_right_eq_restrict_right_left,
      subst restrict_left_Dep_Fun_Rel_rel_restrict_left_eq)
    auto
  also have "... = ?rhs"
    using assms by (subst rel_restrict_left_right_eq_restrict_right_left,
      subst restrict_right_Dep_Fun_Rel_rel_restrict_right_eq)
    (auto elim!: in_codomE t1.left_GaloisE
      simp only: rel_restrict_left_right_eq_restrict_right_left)
  finally show ?thesis .
qed

end


paragraph ‹Function Relator›

context transport_Fun_Rel
begin

corollary Fun_Rel_left_Galois_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) r2"
  and "transitive (≤⇘L2⇙)"
  and "g ≤⇘R⇙ g"
  and "f ⇘L⇙⪅ g"
  shows "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  by (urule tdfr.Dep_Fun_Rel_left_Galois_if_left_GaloisI assms | simp)+

corollary left_Galois_if_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘R⇙) g"
  and "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  by (urule tdfr.left_Galois_if_Dep_Fun_Rel_left_GaloisI assms | simp)+

lemma left_Galois_if_Fun_Rel_left_GaloisI':
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  and "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  by (urule tdfr.left_Galois_if_Dep_Fun_Rel_left_GaloisI' assms | simp)+

corollary left_Galois_iff_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) r2"
  and "transitive (≤⇘L2⇙)"
  and "g ≤⇘R⇙ g"
  shows "f ⇘L⇙⪅ g ⟷ ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  by (urule tdfr.left_Galois_iff_Dep_Fun_Rel_left_GaloisI assms | simp)+


subparagraph ‹Simplification of Restricted Function Relator›

lemma Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  shows "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
  by (urule tdfr.Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI assms
  | simp)+

text ‹Simplification of Restricted Function Relator for Nested Transports›

lemma Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq:
  fixes S :: "'b1 ⇒ 'b2 ⇒ bool"
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  shows "((⇘L1⇙⪅) ⇛ S↾⇘in_dom (≤⇘L2⇙)⇙↿⇘in_codom (≤⇘R2⇙)⇙)↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ =
    ((⇘L1⇙⪅) ⇛ S)↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  by (urule tdfr.Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq assms | simp)+

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemma Dep_Fun_Rel_left_Galois_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x x' y'. x ⇘L1⇙⪅ x' ⟹ in_dom (≤⇘R2 (l1 x) x'⇙) y' ⟹
    (≥⇘L2 x (r1 x')⇙) (r2⇘x (l1 x)⇙ y') ≤ (≥⇘L2 x (r1 x')⇙) (r2⇘x x'⇙ y')"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "f ⇘L⇙⪅ g"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel
  by (intro tdfr.Dep_Fun_Rel_left_Galois_if_left_GaloisI tdfr.left_GaloisI)
  (auto elim!: galois_rel.left_GaloisE in_codomE)

lemma left_Galois_if_Dep_Fun_Rel_left_GaloisI:
  assumes "(tdfr.R ⇛⇩m tdfr.L) r"
  and "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  and "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  using assms unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel
  by (intro tdfr.Galois_Refl_RelI tdfr.left_Galois_if_Dep_Fun_Rel_left_GaloisI)
  (auto simp: in_codom_eq_in_dom_if_reflexive_on_in_field)

lemma left_Galois_iff_Dep_Fun_Rel_left_GaloisI:
  assumes "(tdfr.R ⇛⇩m tdfr.L) r"
  and "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro iffI Dep_Fun_Rel_left_Galois_if_left_GaloisI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI'
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_dom_rightI)
  (auto intro!: left_Galois_if_Dep_Fun_Rel_left_GaloisI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_codom_rightI
    intro: reflexive_on_if_le_pred_if_reflexive_on
      in_field_if_in_dom in_field_if_in_codom)

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and L2_le_unit2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and trans_L2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g" (is "?lhs ⟷ ?rhs")
proof -
  have "(≤⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≤⇘L2 x1 x2⇙) (r2⇘x1 (l1 x1)⇙ y')"
    if hyps: "x1 ≤⇘L1⇙ x2" "in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙) y'" for x1 x2 y'
  proof -
    have "((in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
    proof (intro Fun_Rel_predI)
      from galois_conn1 refl_L1 ‹x1 ≤⇘L1⇙ x2›
        have "x1 ≤⇘L1⇙ x1" "l1 x1 ≤⇘R1⇙ l1 x2" "x1 ⇘L1⇙⪅ l1 x1"
        by (blast intro: t1.left_Galois_left_if_left_relI)+
      fix y' assume "in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙) y'"
      with Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹x1 ≤⇘L1⇙ x1›]
        ‹l1 x1 ≤⇘R1⇙ l1 x2›]
        have "r2⇘x1 (l1 x1)⇙ y' ≤⇘L2 x1 (η⇩1 x2)⇙ r2⇘x1 (l1 x2)⇙ y'"
        using ‹x1 ⇘L1⇙⪅ l1 x1› by (auto dest: in_field_if_in_dom)
      with L2_le_unit2 ‹x1 ≤⇘L1⇙ x2› show "r2⇘x1 (l1 x1)⇙ y' ≤⇘L2 x1 x2⇙ r2⇘x1 (l1 x2)⇙ y'"
        by blast
    qed
    with hyps show ?thesis using trans_L2 by blast
  qed
  then show ?thesis using assms
    using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_GaloisI
      tdfr.mono_wrt_rel_rightI
      tdfr.mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI
      tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_ge_left_rel2_assmI
      tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_mono_assm_in_codom_rightI)
    (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
qed

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | (x1 ≤⇘L1⇙ x2 ∧ x3 ≤⇘L1⇙ η⇩1 x2)) ⇛⇩m (≥)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g" (is "?lhs ⟷ ?rhs")
  using assms by (intro
    left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assmI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_le_assmI)
  auto

corollary left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_mono_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 : ⊤) ⇛⇩m (x2 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | (x1 ≤⇘L1⇙ x2 ∧ x3 ≤⇘L1⇙ η⇩1 x2)) ⇛⇩m (≥)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "(⇘L⇙⪅) = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    iffD1[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI'])
  (auto intro!:
    iffD2[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI'])

lemma left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_le_assmI
    tdfr.reflexive_on_in_field_mono_assm_left2I
    tdfr.left_Galois_iff_Dep_Fun_Rel_left_Galois_left_rel2_unit1_le_assm_if_galois_equivI)
  auto

theorem left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "(⇘L⇙⪅) = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    iffD1[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI])
  (auto intro!: iffD2[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI])

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_galois_equivalenceI)
  auto

corollary left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇛⇩m (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "(⇘L⇙⪅) = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    iffD1[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI])
  (auto intro!: iffD2[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI])

corollary left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅)) f g"
  using assms by (intro left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI
    tdfr.transitive_left2_if_preorder_equivalenceI)
  (auto 5 0)

corollary left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_preorder_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "(⇘L⇙⪅) = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    iffD1[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI'])
  (auto intro!: iffD2[OF left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI'])


subparagraph ‹Simplification of Restricted Function Relator›

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_Galois_if_reflexive_onI:
  assumes "reflexive_on (in_field tdfr.L) tdfr.L"
  and "reflexive_on (in_field tdfr.R) tdfr.R"
  and "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇛⇩m (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙
    = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
  using assms by (auto simp only: left_rel_eq_tdfr_left_rel_if_reflexive_on
      right_rel_eq_tdfr_right_rel_if_reflexive_on
    intro!: tdfr.Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI')

interpretation flip : transport_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.t1.unit ≡ ε⇩1" by (simp only: t1.flip_unit_eq_counit)

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙) (r2⇘(r1 x1') x2'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇛⇩m (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and PERS: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
    "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ partial_equivalence_rel (≤⇘R2 x1' x2'⇙)"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙
    = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
  using assms by (intro
    Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_Galois_if_reflexive_onI
    tdfr.reflexive_on_in_field_left_if_equivalencesI
    flip.reflexive_on_in_field_left_if_equivalencesI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    flip.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI)
  (auto dest!: PERS)


text ‹Simplification of Restricted Function Relator for Nested Transports›

lemma Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq:
  fixes S :: "'a1 ⇒ 'a2 ⇒ 'b1 ⇒ 'b2 ⇒ bool"
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  shows "((x x' ∷ (⇘L1⇙⪅)) ⇛ (S x x')↾⇘in_dom (≤⇘L2 x (r1 x')⇙)⇙↿⇘in_codom (≤⇘R2 (l1 x) x'⇙)⇙)
      ↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ =
    ((x x' ∷ (⇘L1⇙⪅)) ⇛ S x x')↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
    (is "?lhs↾⇘?DL⇙↿⇘?CR⇙ = ?rhs↾⇘?DL⇙↿⇘?CR⇙")
proof (intro ext)
  fix f g
  have "?lhs↾⇘?DL⇙↿⇘?CR⇙ f g ⟷ ?lhs f g ∧ ?DL f ∧ ?CR g" by blast
  also have "... ⟷ ?lhs↾⇘in_dom tdfr.L⇙↿⇘in_codom tdfr.R⇙ f g ∧ ?DL f ∧ ?CR g"
    unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel
    by blast
  also with assms have "... ⟷ ?rhs↾⇘in_dom tdfr.L⇙↿⇘in_codom tdfr.R⇙ f g ∧ ?DL f ∧ ?CR g"
    by (simp only:
      tdfr.Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq)
  also have "... ⟷ ?rhs↾⇘?DL⇙↿⇘?CR⇙ f g"
    unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel
    by blast
  finally show "?lhs↾⇘?DL⇙↿⇘?CR⇙ f g ⟷ ?rhs↾⇘?DL⇙↿⇘?CR⇙ f g" .
qed

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

corollary Fun_Rel_left_Galois_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) (r2)"
  and "transitive (≤⇘L2⇙)"
  and "f ⇘L⇙⪅ g"
  shows "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  by (urule tpdfr.Dep_Fun_Rel_left_Galois_if_left_GaloisI assms | simp)+

interpretation flip : transport_Mono_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2 .

lemma left_Galois_if_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) r2"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  and "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  shows "f ⇘L⇙⪅ g"
  by (urule tpdfr.left_Galois_if_Dep_Fun_Rel_left_GaloisI flip.tfr.mono_wrt_rel_leftI)+
   (urule assms | simp)+

corollary left_Galois_iff_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) (r2)"
  and "transitive (≤⇘L2⇙)"
  and "in_dom (≤⇘L⇙) f"
  and "in_codom (≤⇘R⇙) g"
  shows "f ⇘L⇙⪅ g ⟷ ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
  using assms by (intro iffI Fun_Rel_left_Galois_if_left_GaloisI)
  (auto intro!: left_Galois_if_Fun_Rel_left_GaloisI)

theorem left_Galois_eq_Fun_Rel_left_Galois_restrictI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) r2"
  and "transitive (≤⇘L2⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  using assms by (intro ext iffI rel_restrict_leftI rel_restrict_rightI
    iffD1[OF left_Galois_iff_Fun_Rel_left_GaloisI])
  (auto elim!: tpdfr.left_GaloisE intro!: iffD2[OF left_Galois_iff_Fun_Rel_left_GaloisI])


subparagraph ‹Simplification of Restricted Function Relator›

lemma Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_Galois_if_reflexive_onI:
  assumes "reflexive_on (in_field tfr.tdfr.L) tfr.tdfr.L"
  and "reflexive_on (in_field tfr.tdfr.R) tfr.tdfr.R"
  and "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  shows "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
  using assms by (auto simp only: tpdfr.left_rel_eq_tdfr_left_rel_if_reflexive_on
      tpdfr.right_rel_eq_tdfr_right_rel_if_reflexive_on
    intro!: tfr.Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI)

lemma Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  and "partial_equivalence_rel (≤⇘R2⇙)"
  shows "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
  using assms by (intro
    Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_Galois_if_reflexive_onI
    tfr.reflexive_on_in_field_leftI
    flip.tfr.reflexive_on_in_field_leftI)
  auto


text ‹Simplification of Restricted Function Relator for Nested Transports›

lemma Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq:
  fixes S :: "'b1 ⇒ 'b2 ⇒ bool"
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  shows "((⇘L1⇙⪅) ⇛ S↾⇘in_dom (≤⇘L2⇙)⇙↿⇘in_codom (≤⇘R2⇙)⇙)↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ =
    ((⇘L1⇙⪅) ⇛ S)↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙"
  by (urule tpdfr.Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq assms | simp)+

end


end