Theory Erdos_Milner

theory Erdos_Milner
  imports Partitions

begin

subsection ‹Erdős-Milner theorem›

text ‹P. Erdős and E. C. Milner, A Theorem in the Partition Calculus.
Canadian Math. Bull. 15:4 (1972), 501-505.
Corrigendum, Canadian Math. Bull. 17:2 (1974), 305.›

text ‹The paper defines strong types as satisfying the criteria below.
      It remarks that ordinals satisfy those criteria. Here is a (too complicated) proof.›
proposition strong_ordertype_eq:
  assumes D: "D ⊆ elts β" and "Ord β"
  obtains L where "⋃(List.set L) = D" "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)"
    and "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D"
proof -
  define φ where "φ ≡ inv_into D (ordermap D VWF)"
  then have bij_φ: "bij_betw φ (elts (tp D)) D"
    using D bij_betw_inv_into down ordermap_bij by blast
  have φ_cancel_left: "⋀d. d ∈ D ⟹ φ (ordermap D VWF d) = d"
    by (metis D φ_def bij_betw_inv_into_left down ordermap_bij total_on_VWF wf_VWF)
  have φ_cancel_right: "⋀γ. γ ∈ elts (tp D) ⟹ ordermap D VWF (φ γ) = γ"
    by (metis φ_def f_inv_into_f ordermap_surj subsetD)
  have "small D" "D ⊆ ON"
    using assms down elts_subset_ON [of β] by auto
  then have φ_less_iff: "⋀γ δ. ⟦γ ∈ elts (tp D); δ ∈ elts (tp D)⟧ ⟹ φ γ < φ δ ⟷ γ < δ"
    by (metis φ_def inv_ordermap_VWF_mono_iff inv_ordermap_mono_eq less_V_def)
  obtain αs where "List.set αs ⊆ ON" and "ω_dec αs" and tpD_eq: "tp D = ω_sum αs"
    using Ord_ordertype ω_nf_exists by blast                ― ‹Cantor normal form of the ordertype›
  have ord [simp]: "Ord (αs ! k)" "Ord (ω_sum (take k αs))" if "k < length αs" for k
    using that ‹list.set αs ⊆ ON›
    by (auto simp: dual_order.trans set_take_subset elim: ON_imp_Ord)
  define E where "E ≡ λk. lift (ω_sum (take k αs)) (ω↑(αs!k))"
  define L where "L ≡ map (λk. φ ` (elts (E k))) [0..<length αs]"
  have lengthL [simp]: "length L = length αs"
    by (simp add: L_def)
  have in_elts_E_less: "elts (E k') ≪ elts (E k)" if "k'<k" "k < length αs" for k k'
    ― ‹The ordinals have been partitioned into disjoint intervals›
  proof -
    have ordω: "Ord (ω ↑ αs ! k')"
      using that by auto
    from that id_take_nth_drop [of k' "take k αs"]
    obtain l where "take k αs = take k' αs @ (αs!k') # l"
      by (simp add: min_def)
    then show ?thesis
      using that unfolding E_def lift_def less_sets_def
      by (auto dest!: OrdmemD [OF ordω] intro: less_le_trans)
  qed
  have elts_E: "elts (E k) ⊆ elts (ω_sum αs)"
    if "k < length αs" for k
  proof -
    have "ω ↑ (αs!k) ≤ ω_sum (drop k αs)"
      by (metis that Cons_nth_drop_Suc ω_sum_Cons add_le_cancel_left0)
    then have "(+) (ω_sum (take k αs)) ` elts (ω ↑ (αs!k)) ⊆ elts (ω_sum (take k αs) + ω_sum (drop k αs))"
      by blast
    also have "… = elts (ω_sum αs)"
      using ω_sum_take_drop by auto
    finally show ?thesis
      by (simp add: lift_def E_def)
  qed
  have ω_sum_in_tpD: "ω_sum (take k αs) + γ ∈ elts (tp D)"
    if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k
    using elts_E lift_def that tpD_eq by (auto simp: E_def)
  have Ord_φ: "Ord (φ (ω_sum (take k αs) + γ))"
    if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k
    using ω_sum_in_tpD ‹D ⊆ ON› bij_φ bij_betw_imp_surj_on that by fastforce
  define π where "π ≡ λk. ((λy. odiff y (ω_sum (take k αs))) ∘ ordermap D VWF)"
      ― ‹mapping the segments of @{term D} into some power of @{term ω}›
  have bij_π: "bij_betw (π k) (φ ` elts (E k)) (elts (ω ↑ (αs!k)))"
    if "k < length αs" for k
    using that by (auto simp: bij_betw_def π_def E_def inj_on_def lift_def image_comp ω_sum_in_tpD φ_cancel_right that)
  have π_iff: "π k x < π k y ⟷ (x,y) ∈ VWF"
    if "x ∈ φ ` elts (E k)" "y ∈ φ ` elts (E k)" "k < length αs" for k x y
    using that
    by (auto simp: π_def E_def lift_def ω_sum_in_tpD φ_cancel_right Ord_φ φ_less_iff)
  have tp_E_eq [simp]: "tp (φ ` elts (E k)) = ω↑(αs!k)"
    if k: "k < length αs" for k
    by (metis Ord_ω Ord_oexp π_iff bij_π ord(1) ordertype_VWF_eq_iff replacement small_elts that)
  have tp_L_eq [simp]: "tp (L!k) = ω↑(αs!k)" if "k < length αs" for k
    by (simp add: L_def that)
  have UL_eq_D: "⋃ (list.set L) = D"
  proof (rule antisym)
    show "⋃ (list.set L) ⊆ D"
      by (force simp: L_def tpD_eq bij_betw_apply [OF bij_φ] dest: elts_E)
    show "D ⊆ ⋃ (list.set L)"
    proof
      fix δ
      assume "δ ∈ D"
      then have "ordermap D VWF δ ∈ elts (ω_sum αs)"
        by (metis ‹small D› ordermap_in_ordertype tpD_eq)
      then show "δ ∈ ⋃ (list.set L)"
        using ‹δ ∈ D› φ_cancel_left in_elts_ω_sum
        by (fastforce simp: L_def E_def image_iff lift_def)
    qed
  qed
  show thesis
  proof
    show "indecomposable (tp X)" if "X ∈ list.set L" for X
      using that by (auto simp: L_def indecomposable_ω_power)
  next
    fix M
    assume "M ⊆ D" and *: "⋀X. X ∈ list.set L ⟹ tp X ≤ tp (M ∩ X)"
    show "tp M = tp D"
    proof (rule antisym)
      show "tp M ≤ tp D"
        by (simp add: ‹M ⊆ D› ‹small D› ordertype_VWF_mono)
      define σ where "σ ≡ λX. inv_into (M ∩ X) (ordermap (M ∩ X) VWF)"
                              ― ‹The bijection from an @{term ω}-power into the appropriate segment of @{term M}›
      have bij_σ: "bij_betw (σ X) (elts (tp (M ∩ X))) (M ∩ X)" for X
        unfolding σ_def
        by (meson ‹M ⊆ D› ‹small D› bij_betw_inv_into inf_le1 ordermap_bij smaller_than_small total_on_VWF wf_VWF)
      have Ord_σ: "Ord (σ X α)" if "α ∈ elts (tp (M ∩ X))" for α X
        using ‹D ⊆ ON› ‹M ⊆ D› bij_betw_apply [OF bij_σ] that by blast
      have σ_cancel_right: "⋀γ X. γ ∈ elts (tp (M ∩ X)) ⟹ ordermap (M ∩ X) VWF (σ X γ) = γ"
        by (metis σ_def f_inv_into_f ordermap_surj subsetD)
      have smM: "small (M ∩ X)" for X
        by (meson ‹M ⊆ D› ‹small D› inf_le1 subset_iff_less_eq_V)
      have "∃k < length αs. γ ∈ elts (E k)" if γ: "γ ∈ elts (tp D)" for γ
      proof -
        obtain X where "X ∈ set L" and X: "φ γ ∈ X"
          by (metis UL_eq_D γ Union_iff φ_def in_mono inv_into_into ordermap_surj)
        then have "∃k < length αs. γ ∈ elts (E k) ∧ X = φ ` elts (E k)"
          apply (clarsimp simp: L_def)
          by (metis γ φ_cancel_right elts_E in_mono tpD_eq)
        then show ?thesis
          by blast
      qed
      then obtain K where K: "⋀γ. γ ∈ elts (tp D) ⟹ K γ < length αs ∧ γ ∈ elts (E (K γ))"
        by metis  ― ‹The index from @{term "tp D"} to the appropriate segment number›
      define ψ where "ψ ≡ λd. σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d)"
      show "tp D ≤ tp M"
      proof (rule ordertype_inc_le)
        show "small D" "small M"
          using ‹M ⊆ D› ‹small D› subset_iff_less_eq_V by auto
      next
        fix d' d
        assume xy: "d' ∈ D" "d ∈ D" and "(d',d) ∈ VWF"
        then have "d' < d"
          using ON_imp_Ord ‹D ⊆ ON› by auto
        let ?γ' = "ordermap D VWF d'"
        let ?γ = "ordermap D VWF d"
        have len': "K ?γ' < length αs" and elts': "?γ' ∈ elts (E (K ?γ'))"
          and len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))"
          using K ‹d' ∈ D› ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype)
        have Ord_σL: "Ord (σ (L!k) (π k d))" if "d ∈ φ ` elts (E k)" "k < length αs" for k d
          by (metis (mono_tags) "*" Ord_σ bij_π bij_betw_apply lengthL nth_mem that tp_L_eq vsubsetD)
        have "?γ' < ?γ"
          by (simp add: ‹(d', d) ∈ VWF› ‹small D› ordermap_mono_less xy)
        then have "K ?γ' ≤ K ?γ"
          using elts' elts in_elts_E_less by (meson leI len' less_asym less_sets_def)
        then consider (less) "K ?γ' < K ?γ" | (equal) "K ?γ' = K ?γ"
          by linarith
        then have "σ (L ! K ?γ') (π (K ?γ') d') < σ (L ! K ?γ) (π (K ?γ) d)"
        proof cases
          case less
          obtain †: "σ (L ! K ?γ') (π (K ?γ') d') ∈ M ∩ L ! K ?γ'" "σ (L ! K ?γ) (π (K ?γ) d) ∈ M ∩ L ! K ?γ"
            using elts' elts len' len * [THEN vsubsetD]
            by (metis lengthL φ_cancel_left bij_π bij_σ bij_betw_imp_surj_on imageI nth_mem tp_L_eq xy)
          then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) ∈ elts (E (K ?γ'))" "ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d)) ∈ elts (E (K ?γ))"
            using len' len elts_E tpD_eq
            by (fastforce simp: L_def φ_cancel_right)+
          then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) < ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d))"
            using in_elts_E_less len less by (meson less_sets_def)
          moreover have "σ (L ! K ?γ') (π (K ?γ') d') ∈ D" "σ (L ! K ?γ) (π (K ?γ) d) ∈ D"
            using ‹M ⊆ D› † by auto
          ultimately show ?thesis
            by (metis ‹small D› φ_cancel_left φ_less_iff ordermap_in_ordertype)
        next
          case equal
          have σ_less: "⋀X γ δ. ⟦γ < δ; γ ∈ elts (tp (M ∩ X)); δ ∈ elts (tp (M ∩ X))⟧
                          ⟹ σ X γ < σ X δ"
            by (metis ‹D ⊆ ON› ‹M ⊆ D› σ_def dual_order.trans inv_ordermap_VWF_strict_mono_iff le_infI1 smM)
          have "π (K ?γ) d' < π (K ?γ) d"
            by (metis equal ‹(d', d) ∈ VWF› φ_cancel_left π_iff elts elts' imageI len xy)
          then show ?thesis
            unfolding equal
            by (metis * [THEN vsubsetD] lengthL φ_cancel_left σ_less bij_π 
                 bij_betw_imp_surj_on elts elts' image_eqI len local.equal nth_mem tp_L_eq xy)
        qed
        moreover have "Ord (σ (L ! K ?γ') (π (K ?γ') d'))" "Ord (σ (L ! K ?γ) (π (K ?γ) d))"
          using Ord_σL φ_cancel_left elts len elts' len' xy by fastforce+
        ultimately show "(ψ d', ψ d) ∈ VWF"
          by (simp add: ψ_def)
      next
        show "ψ ` D ⊆ M"
        proof (clarsimp simp: ψ_def)
          fix d
          assume "d ∈ D"
          let ?γ = "ordermap D VWF d"
          have len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))"
            using K ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype)
          have "π (K ?γ) d ∈ elts (tp (L! (K ?γ)))"
            using bij_π [OF len] ‹d ∈ D›
            by (metis φ_cancel_left bij_betw_apply elts imageI len tp_L_eq)
          then show "σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d) ∈ M"
            by (metis "*" lengthL Int_iff bij_σ bij_betw_apply len nth_mem vsubsetD) 
        qed
      qed auto
    qed
  qed (simp add: UL_eq_D)
qed


text ‹The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974›

proposition indecomposable_imp_Ex_less_sets:
  assumes indec: "indecomposable α" and "α ≥ ω" 
    and A: "tp A = α" "small A" "A ⊆ ON"
    and "x ∈ A" and A1: "tp A1 = α" "A1 ⊆ A"
  obtains A2 where "tp A2 = α" "A2 ⊆ A1" "{x} ≪ A2"
proof -
  have "Ord α"
    using indec indecomposable_imp_Ord by blast
  have "Limit α"
    by (meson ω_gt1 assms indec indecomposable_imp_Limit less_le_trans)
  define φ where "φ ≡ inv_into A (ordermap A VWF)"
  then have bij_φ: "bij_betw φ (elts α) A"
    using A bij_betw_inv_into down ordermap_bij by blast
  have bij_om: "bij_betw (ordermap A VWF) A (elts α)"
    using A down ordermap_bij by blast
  define γ where "γ ≡ ordermap A VWF x"
  have γ: "γ ∈ elts α"
    unfolding γ_def using A ‹x ∈ A› down by auto
  then have "Ord γ"
    using Ord_in_Ord ‹Ord α› by blast
  define B where "B ≡ φ ` (elts (succ γ))"
  have B: "{y ∈ A. ordermap A VWF y ≤ ordermap A VWF x} ⊆ B"
    apply (clarsimp simp add: B_def γ_def image_iff φ_def)
    by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD)
  show thesis
  proof
    have "small A1"
      by (meson ‹small A› A1 smaller_than_small)
    then have "tp (A1 - B) ≤ tp A1"
      by (simp add: ordertype_VWF_mono)
    moreover have "tp (A1 - B) ≥ α"
    proof -
      have "¬ (α ≤ tp B)"
        unfolding B_def
      proof (subst ordertype_VWF_inc_eq)
        show "elts (succ  γ) ⊆ ON"
          by (auto simp: γ_def ordertype_VWF_inc_eq intro: Ord_in_Ord)
        have sub: "elts (succ  γ) ⊆ elts α"
          using Ord_trans γ ‹Ord α› by auto
        then show "φ ` elts (succ  γ) ⊆ ON"
          using ‹A ⊆ ON› bij_φ bij_betw_imp_surj_on by blast
        have "succ γ ∈ elts α"
          using γ Limit_def ‹Limit α› by blast
        with A sub show "φ u < φ v"
          if "u ∈ elts (succ  γ)" and "v ∈ elts (succ  γ)" and "u < v" for u v
          by (metis φ_def inv_ordermap_VWF_strict_mono_iff subsetD that)
        show "¬ α ≤ tp (elts (succ  γ))"
          by (metis Limit_def Ord_succ γ ‹Limit α› ‹Ord γ› mem_not_refl ordertype_eq_Ord vsubsetD)
      qed auto
      then show ?thesis
        using indecomposable_ordertype_ge [OF indec, of A1 B] ‹small A1› A1 by (auto simp: B_def)
    qed
    ultimately show "tp (A1 - B) = α"
      using A1 by blast
    have "{x} ≪ (A - B)"
      using assms B 
      apply (clarsimp simp: less_sets_def φ_def subset_iff)
      by (metis Ord_not_le VWF_iff_Ord_less less_V_def order_refl ordermap_mono_less trans_VWF wf_VWF)
    with ‹A1 ⊆ A› show "{x} ≪ (A1 - B)" by auto
  qed auto
qed


text ‹the main theorem, from which they derive the headline result›
theorem Erdos_Milner_aux:
  assumes part: "partn_lst_VWF α [k, γ] 2"
    and indec: "indecomposable α" and "k > 1" "Ord γ" and β: "β ∈ elts ω1"
  shows "partn_lst_VWF (α*β) [ord_of_nat (2*k), min γ (ω*β)] 2"
proof (cases "α≤1 ∨ β=0")
  case True
  have "Ord α"
    using indec indecomposable_def by blast
  show ?thesis
  proof (cases "β=0")
    case True then show ?thesis
      by (simp add: partn_lst_triv0 [where i=1])
  next
    case False
    then consider (0) "α=0" | (1) "α=1"
      by (metis Ord_0 OrdmemD True ‹Ord α› mem_0_Ord one_V_def order.antisym succ_le_iff)
    then show ?thesis
    proof cases
      case 0
      with part show ?thesis
        by (force simp add: partn_lst_def nsets_empty_iff less_Suc_eq)
    next
      case 1
      then obtain "Ord β"
        by (meson ON_imp_Ord Ord_ω1 True β elts_subset_ON)
      then obtain i where "i < Suc (Suc 0)" "[ord_of_nat k, γ] ! i ≤ α"
        using partn_lst_VWF_nontriv [OF part] 1 by auto
      then have "γ ≤ 1"
        using ‹α=1› ‹k > 1› by (fastforce simp: less_Suc_eq)
      then have "min γ (ω*β) ≤ 1"
        by (metis Ord_1 Ord_ω Ord_linear_le Ord_mult ‹Ord β› min_def order_trans)
      then show ?thesis
        using False by (auto simp: True ‹Ord β› ‹β≠0› ‹α=1› intro!: partn_lst_triv1 [where i=1])
    qed
  qed
next
  case False
  then have "α ≥ ω"
    by (meson Ord_1 Ord_not_less indec indecomposable_def indecomposable_imp_Limit omega_le_Limit)
  have "0 ∈ elts β" "β ≠ 0"
    using False Ord_ω1 Ord_in_Ord β mem_0_Ord by blast+
  show ?thesis
    unfolding partn_lst_def
  proof clarsimp
    fix f
    assume "f ∈ [elts (α*β)]⇗2⇖ → {..<Suc (Suc 0)}"
    then have f: "f ∈ [elts (α*β)]⇗2⇖ → {..<2::nat}"
      by (simp add: eval_nat_numeral)
    obtain ord [iff]: "Ord α" "Ord β" "Ord (α*β)"
      using Ord_ω1 Ord_in_Ord β indec indecomposable_imp_Ord Ord_mult by blast
    have *: False
      if i [rule_format]: "∀H. tp H = ord_of_nat (2*k) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {0}"
        and ii [rule_format]: "∀H. tp H = γ ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}"
        and iii [rule_format]: "∀H. tp H = (ω*β) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}"
    proof -
      have Ak0: "∃X ∈ [A]⇗k⇖. f ` [X]⇗2⇖ ⊆ {0}" ―‹remark (8) about @{term"A ⊆ S"}›
        if A_αβ: "A ⊆ elts (α*β)" and ot: "tp A ≥ α" for A
      proof -
        let ?g = "inv_into A (ordermap A VWF)"
        have "small A"
          using down that by auto
        then have inj_g: "inj_on ?g (elts α)"
          by (meson inj_on_inv_into less_eq_V_def ordermap_surj ot subset_trans)
        have om_A_less: "⋀x y. ⟦x ∈ A; y ∈ A; x < y⟧ ⟹ ordermap A VWF x < ordermap A VWF y"
          using ord
          by (meson A_αβ Ord_in_Ord VWF_iff_Ord_less ‹small A› in_mono ordermap_mono_less trans_VWF wf_VWF)
        have α_sub: "elts α ⊆ ordermap A VWF ` A"
          by (metis ‹small A› elts_of_set less_eq_V_def ordertype_def ot replacement)
        have g: "?g ∈ elts α → elts (α*β)"
          by (meson A_αβ Pi_I' α_sub inv_into_into subset_eq)
        then have fg: "f ∘ (λX. ?g ` X) ∈ [elts α]⇗2⇖ → {..<2}"
          by (rule nsets_compose_image_funcset [OF f _ inj_g])
        obtain i H where "i < 2" "H ⊆ elts α"
          and ot_eq: "tp H = [k,γ]!i" "(f ∘ (λX. ?g ` X)) ` (nsets H 2) ⊆ {i}"
          using ii partn_lst_E [OF part fg] by (auto simp: eval_nat_numeral)
        then consider (0) "i=0" | (1) "i=1"
          by linarith
        then show ?thesis
        proof cases
          case 0
          then have "f ` [inv_into A (ordermap A VWF) ` H]⇗2⇖ ⊆ {0}"
            using ot_eq ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] inj_on_inv_into elim!: nset_image_obtains)
          moreover have "finite H ∧ card H = k"
            using 0 ot_eq ‹H ⊆ elts α› down by (simp add: finite_ordertype_eq_card)
          then have "inv_into A (ordermap A VWF) ` H ∈ [A]⇗k⇖"
            using ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] card_image inj_on_inv_into inv_into_into)
          ultimately show ?thesis
            by blast
        next
          case 1
          have gH: "?g ` H ⊆ elts (α*β)"
            by (metis A_αβ α_sub ‹H ⊆ elts α› image_subsetI inv_into_into subset_eq)
          have g_less: "?g x < ?g y" if "x < y" "x ∈ elts α" "y ∈ elts α" for x y
            using Pi_mem [OF g] ord that
            by (meson A_αβ Ord_in_Ord Ord_not_le ‹small A› dual_order.trans elts_subset_ON inv_ordermap_VWF_mono_le ot vsubsetD)
          have [simp]: "tp (?g ` H) = tp H"
            by (meson ‹H ⊆ elts α› ord down dual_order.trans elts_subset_ON gH g_less ordertype_VWF_inc_eq subsetD)
          show ?thesis
            using ii [of "?g ` H"] subset_inj_on [OF inj_g ‹H ⊆ elts α›] ot_eq 1 
            by (auto simp: gH elim!: nset_image_obtains)
        qed
      qed
      define K where "K ≡ λi x. {y ∈ elts (α*β). x ≠ y ∧ f{x,y} = i}"
      have small_K: "small (K i x)" for i x
        by (simp add: K_def)
      define KI where "KI ≡ λi X. (⋂x∈X. K i x)"
      have KI_disj_self: "X ∩ KI i X = {}" for i X
        by (auto simp: KI_def K_def)
      define M where "M ≡ λD 𝔄 x. {ν::V. ν ∈ D ∧ tp (K 1 x ∩ 𝔄 ν) ≥ α}"
      have M_sub_D: "M D 𝔄 x ⊆ D" for D 𝔄 x
        by (auto simp: M_def)
      have small_M [simp]: "small (M D 𝔄 x)" if "small D" for D 𝔄 x
        by (simp add: M_def that)
      have 9: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α" (is "ordertype ?AD _ ≥ α")
        if inD: "indecomposable (tp D)" and D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α"
          and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}"  for D A 𝔄
          ―‹remark (9), assuming an indecomposable order type›
      proof (rule ccontr)
        define A' where "A' ≡ {x ∈ A. ¬ tp (M D 𝔄 x) ≥ tp D}"
        have small [iff]: "small A" "small D"
          using A D down by (auto simp: M_def)
        have small_𝔄: "small (𝔄 δ)" if "δ ∈ D" for δ
          using that 𝔄 by (auto simp: Pi_iff subset_iff_less_eq_V)
        assume not_α_le: "¬ α ≤ tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D}"
        moreover
        obtain "small A" "small A'" "A' ⊆ A" and A'_sub: "A' ⊆ elts (α*β)"
          using A'_def A down by auto
        moreover have "A' = A - ?AD"
          by (force simp: A'_def)
        ultimately have A'_ge: "tp A' ≥ α"
          by (metis (no_types, lifting) dual_order.refl indec indecomposable_ordertype_eq mem_Collect_eq subsetI tpA)
        obtain X where "X ⊆ A'" "finite X" "card X = k" and fX0: "f ` [X]⇗2⇖ ⊆ {0}"
          using Ak0 [OF A'_sub A'_ge] by (auto simp: nsets_def [of _ k])
        then have ‡: "¬ tp (M D 𝔄 x) ≥ tp D" if "x ∈ X" for x
          using that by (auto simp: A'_def)
        obtain x where "x ∈ X"
          using ‹card X = k› ‹k>1› by fastforce
        have "¬ D ⊆ (⋃ x∈X. M D 𝔄 x)"
        proof
          assume not: "D ⊆ (⋃x∈X. M D 𝔄 x)"
          have "∃X∈M D 𝔄 ` X. tp D ≤ tp X"
          proof (rule indecomposable_ordertype_finite_ge [OF inD])
            show "M D 𝔄 ` X ≠ {}"
              using A'_def A'_ge not not_α_le by auto
            show "small (⋃ (M D 𝔄 ` X))"
              using ‹finite X› by (simp add: finite_imp_small)
          qed (use ‹finite X› not in auto)
          then show False
            by (simp add: ‡)
        qed
        then obtain ν where "ν ∈ D" and ν: "ν ∉ (⋃ x∈X. M D 𝔄 x)"
          by blast
        define 𝒜 where "𝒜 ≡ {KI 0 X ∩ 𝔄 ν, ⋃x∈X. K 1 x ∩ 𝔄 ν, X ∩ 𝔄 ν}"
        have αβ: "X ⊆ elts (α*β)" "𝔄 ν ⊆ elts (α*β)"
          using A'_sub ‹X ⊆ A'› 𝔄 ‹ν ∈ D› by auto
        then have "KI 0 X ∪ (⋃x∈X. K 1 x) ∪ X = elts (α*β)"
          using ‹x ∈ X› f by (force simp: K_def KI_def Pi_iff less_2_cases_iff)
        with αβ have 𝔄ν_𝒜: "finite 𝒜" "𝔄 ν ⊆ ⋃𝒜"
          by (auto simp: 𝒜_def)
        then have "¬ tp (K 1 x ∩ 𝔄 ν) ≥ α" if "x ∈ X" for x
          using that ‹ν ∈ D› ν ‹k > 1› ‹card X = k› by (fastforce simp: M_def)
        moreover have sm_K1: "small (⋃x∈X. K 1 x ∩ 𝔄 ν)"
          by (meson Finite_V Int_lower2 ‹ν ∈ D› ‹finite X› small_𝔄 small_UN smaller_than_small)
        ultimately have not1: "¬ tp (⋃x∈X. K 1 x ∩ 𝔄 ν) ≥ α"
          using ‹finite X› ‹x ∈ X› indecomposable_ordertype_finite_ge [OF indec, of "(λx. K 1 x ∩ 𝔄 ν) ` X"] by blast
        moreover have "¬ tp (X ∩ 𝔄 ν) ≥ α"
          using ‹finite X› ‹α ≥ ω›
          by (meson finite_Int mem_not_refl ordertype_VWF_ω vsubsetD)
        moreover have "α ≤ tp (𝔄 ν)"
          using 𝔄 ‹ν ∈ D› small_𝔄 by fastforce+
        moreover have "small (⋃ 𝒜)"
          using ‹ν ∈ D› small_𝔄 by (fastforce simp: 𝒜_def intro: smaller_than_small sm_K1)
        ultimately have K0𝔄_ge: "tp (KI 0 X ∩ 𝔄 ν) ≥ α"
          using indecomposable_ordertype_finite_ge [OF indec 𝔄ν_𝒜] by (auto simp: 𝒜_def)
        have 𝔄ν: "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α"
          using ‹ν ∈ D› 𝔄 by blast+
        then obtain Y where Ysub: "Y ⊆ KI 0 X ∩ 𝔄 ν" and "finite Y" "card Y = k" and fY0: "f ` [Y]⇗2⇖ ⊆ {0}"
          using Ak0 [OF _ K0𝔄_ge] by (auto simp: nsets_def [of _ k])
        have †: "X ∩ Y = {}"
          using Ysub KI_disj_self by blast
        then have "card (X ∪ Y) = 2*k"
          by (simp add: ‹card X = k› ‹card Y = k› ‹finite X› ‹finite Y› card_Un_disjoint)
        moreover have "X ∪ Y ⊆ elts (α*β)"
          using A'_sub ‹X ⊆ A'› 𝔄ν(1) ‹Y ⊆ KI 0 X ∩ 𝔄 ν› by auto
        moreover have "f ` [X ∪ Y]⇗2⇖ ⊆ {0}"
          using fX0 fY0 Ysub by (auto simp: † nsets_disjoint_2 image_Un image_UN KI_def K_def)
        ultimately show False
          using i ‹finite X› ‹finite Y› ordertype_VWF_finite_nat by auto
      qed
      have IX: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α"
        if D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α"
          and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}" for D A 𝔄
          ―‹remark (9) for any order type›
      proof -
        obtain L where UL: "⋃(List.set L) ⊆ D"
          and indL: "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)"
          and eqL: "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D"
          using ord by (metis strong_ordertype_eq D order_refl)
        obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α"
          and "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X"
          using UL indL
        proof (induction L arbitrary: thesis)
          case (Cons X L)
          then obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α" and "X ⊆ D"
            and ge_X: "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X" by auto
          then have tp_A'': "tp A'' = α"
            by (metis A antisym down ordertype_VWF_mono tpA)
          have ge_α: "tp {x ∈ A''. tp (M X 𝔄 x) ≥ tp X} ≥ α"
            by (rule 9) (use A A'' tp_A'' Cons.prems ‹D ⊆ elts β› ‹X ⊆ D› 𝔄 in auto)
          let ?A = "{x ∈ A''. tp (M D 𝔄 x ∩ X) ≥ tp X}"
          have M_eq: "M D 𝔄 x ∩ X = M X 𝔄 x" if "x ∈ A''" for x
            using that ‹X ⊆ D› by (auto simp: M_def)
          show thesis
          proof (rule Cons.prems)
            show "α ≤ tp ?A"
              using ge_α by (simp add: M_eq cong: conj_cong)
            show "tp Y ≤ tp (M D 𝔄 x ∩ Y)" if "x ∈ ?A" "Y ∈ list.set (X # L)" for x Y
              using that ge_X by force
          qed (use A'' in auto)
        qed (use tpA in auto)
        then have tp_M_ge: "tp (M D 𝔄 x) ≥ tp D" if "x ∈ A''" for x
          using eqL that by (auto simp: M_def)
        have "α ≤ tp A''"
          by (simp add: A'')
        also have "… ≤ tp {x ∈ A''. tp (M D 𝔄 x) ≥ tp D}"
          by (metis (mono_tags, lifting) tp_M_ge eq_iff mem_Collect_eq subsetI)
        also have "… ≤ tp {x ∈ A. tp D ≤ tp (M D 𝔄 x)}"
          by (rule ordertype_mono) (use A'' A down in auto)
        finally show ?thesis .
      qed
      have IX': "tp {x ∈ A'. tp (K 1 x ∩ A) ≥ α} ≥ α"
        if A: "A ⊆ elts (α*β)" "tp A = α" and A': "A' ⊆ elts (α*β)" "tp A' = α" for A A'
      proof -
        have ‡: "α ≤ tp (K 1 t ∩ A)" if "1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 t ∩ A)}" for t
          using that
          by (metis Collect_empty_eq less_eq_V_0_iff ordertype_empty zero_neq_one)
        have "tp {x ∈ A'. 1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 x ∩ A)}}
            ≤ tp {x ∈ A'. α ≤ tp (K 1 x ∩ A)}"
          by (rule ordertype_mono) (use "‡" A' in ‹auto simp: down›)
        then show ?thesis
          using IX [of "{0}" A' "λx. A"] that ‹0 ∈ elts β› by (force simp: M_def)
      qed

      have 10: "∃x0 ∈ A. ∃g ∈ elts β → elts β. strict_mono_on (elts β) g ∧ (∀ν ∈ F. g ν = ν)
                                      ∧ (∀ν ∈ elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) ≥ α)"
        if F: "finite F" "F ⊆ elts β"
          and A: "A ⊆ elts (α*β)" "tp A = α"
          and 𝔄: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}"
        for F A 𝔄
      proof -
        define p where "p ≡ card F"
        have "β ∉ F"
          using that by auto
        then obtain ι :: "nat ⇒ V" where bijι: "bij_betw ι {..p} (insert β F)" and monι: "strict_mono_on {..p} ι"
          using ZFC_Cardinals.ex_bij_betw_strict_mono_card [of "insert β F"] elts_subset_ON ‹Ord β› F
          by (simp add: p_def lessThan_Suc_atMost) blast
        have less_ι_I: "ι k < ι l" if "k < l" "l ≤ p" for k l
          using monι that by (auto simp: strict_mono_on_def)
        then have less_ι_D: "k < l" if "ι k < ι l" "k ≤ p" for k l
          by (metis less_asym linorder_neqE_nat that)
        have Ord_ι: "Ord (ι k)" if "k ≤ p" for k
          by (metis (no_types, lifting) ON_imp_Ord atMost_iff insert_subset mem_Collect_eq order_trans  ‹F ⊆ elts β› bijι bij_betwE elts_subset_ON ‹Ord β› that)
        have le_ι0 [simp]: "⋀j. j ≤ p ⟹ ι 0 ≤ ι j"
          by (metis eq_refl leI le_0_eq less_ι_I less_imp_le)
        have le_ι: "ι i ≤ ι (j - Suc 0)" if "i < j" "j ≤ p" for i j
        proof (cases i)
          case 0 then show ?thesis
            using le_ι0 that by auto
        next
          case (Suc i') then show ?thesis
            by (metis (no_types, opaque_lifting) Suc_pred le_less less_Suc_eq less_Suc_eq_0_disj less_ι_I not_less_eq that)
        qed

        have [simp]: "ι p = β"
        proof -
          obtain k where k: "ι k = β" "k ≤ p"
            by (meson atMost_iff bijι bij_betw_iff_bijections insertI1)
          then have "k = p ∨ k < p"
            by linarith
          then show ?thesis
            using bijι ord k that(2)
            by (metis OrdmemD atMost_iff bij_betw_iff_bijections insert_iff leD less_ι_D order_refl subsetD)
        qed

        have F_imp_Ex: "∃k < p. ξ = ι k" if "ξ ∈ F" for ξ
        proof -
          obtain k where k: "k ≤ p" "ξ = ι k"
            by (metis ‹ξ ∈ F› atMost_iff bijι bij_betw_def imageE insert_iff)
          then show ?thesis
            using ‹β ∉ F› ‹ι p = β› le_imp_less_or_eq that by blast
        qed
        have F_imp_ge: "ξ ≥ ι 0" if "ξ ∈ F" for ξ
          using F_imp_Ex [OF that] by (metis dual_order.order_iff_strict le0 less_ι_I)
        define D where "D ≡ λk. (if k=0 then {..<ι 0} else {ι (k-1)<..<ι k}) ∩ elts β"
        have Dβ: "D k ⊆ elts β" for k
          by (auto simp: D_def)
        then have small_D [simp]: "small (D k)" for k
          by (meson down)
        have M_Int_D: "M (elts β) 𝔄 x ∩ D k = M (D k) 𝔄 x" if "k ≤ p" for x k
          using Dβ by (auto simp: M_def)
        have ι_le_if_D: "ι k ≤ μ" if "μ ∈ D (Suc k)" for μ k
          using that by (simp add: D_def order.order_iff_strict)
        have mono_D: "D i ≪ D j" if "i < j" "j ≤ p" for i j
        proof (cases j)
          case (Suc j')
          with that show ?thesis
            apply (simp add: less_sets_def D_def Ball_def)
            by (metis One_nat_def diff_Suc_1 le_ι less_le_trans less_trans)
        qed (use that in auto)
        then have disjnt_DD: "disjnt (D i) (D j)" if "i ≠ j" "i ≤ p" "j ≤ p" for i j
          by (meson disjnt_sym less_linear less_sets_imp_disjnt that)
        have UN_D_eq: "(⋃l ≤ k. D l) = {..<ι k} ∩ (elts β - F)" if "k ≤ p" for k
          using that
        proof (induction k)
          case 0
          then show ?case
            by (auto simp: D_def F_imp_ge leD)
        next
          case (Suc k)
          have "D (Suc k) ∪ {..<ι k} ∩ (elts β - F) = {..<ι (Suc k)} ∩ (elts β - F)"
            (is "?lhs = ?rhs")
          proof
            show "?lhs ⊆ ?rhs"
              using Suc.prems
              by (auto simp: D_def if_split_mem2 intro: less_ι_I less_trans dest!: less_ι_D F_imp_Ex)
            have "⋀x. ⟦x < ι (Suc k); x ∈ elts β; x ∉ F; ι k ≤ x⟧ ⟹ ι k < x"
              using Suc.prems ‹F ⊆ elts β› bijι le_imp_less_or_eq
              by (fastforce simp: bij_betw_iff_bijections)
            then show "?rhs ⊆ ?lhs"
              using Suc.prems by (auto simp: D_def Ord_not_less Ord_in_Ord [OF ‹Ord β›] Ord_ι if_split_mem2)
          qed
          then
          show ?case
            using Suc by (simp add: atMost_Suc)
        qed
        have β_decomp: "elts β = F ∪ (⋃k ≤ p. D k)"
          using ‹F ⊆ elts β› OrdmemD [OF ‹Ord β›] by (auto simp: UN_D_eq)
        define βidx where "βidx ≡ λν. @k. ν ∈ D k ∧ k ≤ p"
        have βidx: "ν ∈ D (βidx ν) ∧ βidx ν ≤ p" if "ν ∈ elts β - F" for ν
          using that by (force simp: βidx_def β_decomp intro: someI_ex del: conjI)
        have any_imp_βidx: "k = βidx ν" if "ν ∈ D k" "k ≤ p" for k ν
        proof (rule ccontr)
          assume non: "k ≠ βidx ν"
          have "ν ∉ F"
            using that UN_D_eq by auto
          then show False
            using disjnt_DD [OF non] by (metis Dβ Diff_iff βidx disjnt_iff subsetD that)
        qed
        have "∃A'. A' ⊆ A ∧ tp A' = α ∧ (∀x ∈ A'. F ⊆ M (elts β) 𝔄 x)"
          using F
        proof induction
          case (insert ν F)
          then obtain A' where "A' ⊆ A" and A': "A' ⊆ elts (α*β)" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x"
            using A(1) by auto
          define A'' where "A'' ≡ {x ∈ A'. α ≤ tp (K 1 x ∩ 𝔄 ν)}"
          have "ν ∈ elts β" "F ⊆ elts β"
            using insert by auto
          note ordertype_eq_Ord [OF ‹Ord β›, simp]
          show ?case
          proof (intro exI conjI)
            show "A'' ⊆ A"
              using ‹A' ⊆ A› by (auto simp: A''_def)
            show "tp A'' = α"
            proof (rule antisym)
              show "tp A'' ≤ α"
                using ‹A'' ⊆ A› down ordertype_VWF_mono A by blast
              have "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α"
                using 𝔄 ‹ν ∈ elts β› by auto
              then show "α ≤ tp A''"
                using IX' [OF _ _ A'] by (simp add: A''_def)
            qed
            show "∀x∈A''. insert ν F ⊆ M (elts β) 𝔄 x"
              using A''_def FN M_def ‹ν ∈ elts β› by blast
          qed
        qed (use A in auto)
        then obtain A' where A': "A' ⊆ A" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x"
          by metis
        have False
          if *: "⋀x0 g. ⟦x0 ∈ A; g ∈ elts β → elts β; strict_mono_on (elts β) g⟧
                   ⟹ (∃ν∈F. g ν ≠ ν) ∨ (∃ν∈elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) < α)"
        proof -
          { fix x       ― ‹construction of the monotone map @{term g} mentioned above›
            assume "x ∈ A'"
            with A' have "x ∈ A" by blast
            have "∃k. k ≤ p ∧ tp (M (D k) 𝔄 x) < tp (D k)" (is "?P")
            proof (rule ccontr)
              assume "¬ ?P"
              then have le: "tp (D k) ≤ tp (M (D k) 𝔄 x)" if "k ≤ p" for k
                by (meson Ord_linear2 Ord_ordertype that)
              have "∃f∈D k → M (D k) 𝔄 x. inj_on f (D k) ∧ (strict_mono_on (D k) f)"
                if "k ≤ p" for k
                using le [OF that] that VWF_iff_Ord_less
                apply (clarsimp simp: ordertype_le_ordertype strict_mono_on_def)
                by (metis (full_types) Dβ M_sub_D Ord_in_Ord PiE VWF_iff_Ord_less ord(2) subsetD)
              then obtain h where fun_h: "⋀k. k ≤ p ⟹ h k ∈ D k → M (D k) 𝔄 x"
                and inj_h: "⋀k. k ≤ p ⟹ inj_on (h k) (D k)"
                and mono_h: "⋀k x y. k ≤ p ⟹ strict_mono_on (D k) (h k)"
                by metis
              then have fun_hD: "⋀k. k ≤ p ⟹ h k ∈ D k → D k"
                by (auto simp: M_def)
              have h_increasing: "ν ≤ h k ν"
                if "k ≤ p" "ν ∈ D k" for k ν 
                by (meson Dβ Ord_mono_imp_increasing ord dual_order.trans elts_subset_ON fun_hD mono_h that)
              define g where "g ≡ λν. if ν ∈ F then ν else h (βidx ν) ν"
              have [simp]: "g ν = ν" if "ν ∈ F" for ν
                using that by (auto simp: g_def)
              have fun_g: "g ∈ elts β → elts β"
              proof (rule Pi_I)
                fix x assume "x ∈ elts β"
                then have "x ∈ D (βidx x)" "βidx x ≤ p" if "x ∉ F"
                  using that by (auto simp: βidx)
                then show "g x ∈ elts β"
                  by (metis fun_h Dβ M_sub_D ‹x ∈ elts β› PiE g_def subsetD)
              qed
              have h_in_D: "h (βidx ν) ν ∈ D (βidx ν)" if "ν ∉ F" "ν ∈ elts β" for ν
                using βidx fun_hD that by fastforce
              have 1: "ι k < h (βidx ν) ν"
                if "k < p" and ν: "ν ∉ F" "ν ∈ elts β" and "ι k < ν" for k ν
                by (meson that h_in_D [OF ν] βidx DiffI h_increasing order_less_le_trans)
              moreover have 2: "h (βidx μ) μ < ι k"
                if μ: "μ ∉ F" "μ ∈ elts β" and "k < p" "μ < ι k" for μ k
              proof -
                have "βidx μ ≤ k"
                proof (rule ccontr)
                  assume "¬ βidx μ ≤ k"
                  then have "k < βidx μ"
                    by linarith
                  then show False
                    using ι_le_if_D βidx that by (metis Diff_iff Suc_pred le0 leD le_ι le_less_trans)
                qed
                then show ?thesis
                  using that h_in_D [OF μ]
                  by (smt (verit, best) Int_lower1 UN_D_eq UN_I atMost_iff lessThan_iff less_imp_le subset_eq)
              qed
              moreover have "h (βidx μ) μ < h (βidx ν) ν"
                if μ: "μ ∉ F" "μ ∈ elts β" and ν: "ν ∉ F" "ν ∈ elts β" and "μ < ν" for μ ν
              proof -
                have le: "βidx μ ≤ βidx ν" if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
                  by (metis 2 DiffI βidx μ ν ‹μ < ν› order.strict_trans h_increasing leI le_ι order_less_asym order_less_le_trans that)
                have "h 0 μ < h 0 ν" if "βidx μ = 0" "βidx ν = 0"
                  using that mono_h unfolding strict_mono_on_def
                  by (metis Diff_iff βidx μ ν ‹μ < ν›)
                moreover have "h 0 μ < h (βidx ν) ν"
                  if "0 < βidx ν" "h 0 μ < ι 0" and "ι (βidx ν - Suc 0) < h (βidx ν) ν"
                  by (meson DiffI βidx ν le_ι le_less_trans less_le_not_le that)
                moreover have "βidx ν ≠ 0"
                  if "0 < βidx μ" "h 0 ν < ι 0" "ι (βidx μ - Suc 0) < h (βidx μ) μ"
                  using le le_0_eq that by fastforce
                moreover have "h (βidx μ) μ < h (βidx ν) ν"
                  if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
                    "h (βidx μ) μ < ι (βidx μ)" "ι (βidx ν - Suc 0) < h (βidx ν) ν"
                  using mono_h unfolding strict_mono_on_def
                  by (metis le Diff_iff βidx μ ν ‹μ < ν› le_ι le_less le_less_trans that)
                ultimately show  ?thesis
                  using h_in_D [OF μ] h_in_D [OF ν] by (simp add: D_def split: if_split_asm)
              qed
              ultimately have sm_g: "strict_mono_on (elts β) g"
                by (auto simp: g_def strict_mono_on_def dest!: F_imp_Ex)
              have False if "ν ∈ elts β" and ν: "tp (K 1 x ∩ 𝔄 (g ν)) < α" for ν
              proof -
                have "F ⊆ M (elts β) 𝔄 x"
                  by (meson FN ‹x ∈ A'›)
                then have False if "tp (K (Suc 0) x ∩ 𝔄 ν) < α" "ν ∈ F"
                  using that by (auto simp: M_def)
                moreover have False if "tp (K (Suc 0) x ∩ 𝔄 (g ν)) < α" "ν ∈ D k" "k ≤ p" "ν ∉ F" for k
                proof -
                  have "h (βidx ν) ν ∈ M (D (βidx ν)) 𝔄 x"
                    using fun_h βidx ‹ν ∈ elts β› ‹ν ∉ F› by auto
                  then show False
                    using that by (simp add: M_def g_def leD)
                qed
                ultimately show False
                  using ‹ν ∈ elts β› ν by (force simp: β_decomp)
              qed
              then show False
                using * [OF ‹x ∈ A› fun_g sm_g] by auto
            qed
            then have "∃l. l ≤ p ∧ tp (M (elts β) 𝔄 x ∩ D l) < tp (D l)"
              using M_Int_D by auto
          }
          then obtain l where lp: "⋀x. x ∈ A'⟹ l x ≤ p"
            and lless: "⋀x. x ∈ A'⟹ tp (M (elts β) 𝔄 x ∩ D (l x)) < tp (D (l x))"
            by metis
          obtain A'' L where "A'' ⊆ A'" and A'': "A'' ⊆ elts (α*β)" "tp A'' = α" and lL: "⋀x. x ∈ A'' ⟹ l x = L"
          proof -
            have eq: "A' = (⋃i≤p. {x ∈ A'. l x = i})"
              using lp by auto
            have "∃X∈(λi. {x ∈ A'. l x = i}) ` {..p}. α ≤ tp X"
            proof (rule indecomposable_ordertype_finite_ge [OF indec])
              show "small (⋃i≤p. {x ∈ A'. l x = i})"
                by (metis A'(1) A(1) eq down smaller_than_small)
            qed (use A' eq in auto)
            then show thesis
            proof
              fix A''
              assume A'': "A'' ∈ (λi. {x ∈ A'. l x = i}) ` {..p}" and "α ≤ tp A''"
              then obtain L where L: "⋀x. x ∈ A'' ⟹ l x = L"
                by auto
              have "A'' ⊆ A'"
                using A'' by force
              then have "tp A'' ≤ tp A'"
                by (meson A' A down order_trans ordertype_VWF_mono)
              with ‹α ≤ tp A''› have "tp A'' = α"
                using A'(2) by auto
              moreover have "A'' ⊆ elts (α*β)"
                using A' A ‹A'' ⊆ A'› by auto
              ultimately show thesis
                using L that [OF ‹A'' ⊆ A'›] by blast
            qed
          qed
          have 𝔄D: "𝔄 ∈ D L → {X. X ⊆ elts (α*β) ∧ tp X = α}"
            using 𝔄 Dβ by blast
          have α: "α ≤ tp {x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)}"
            using IX [OF Dβ A'' 𝔄D] by simp
          have "M (elts β) 𝔄 x ∩ D L = M (D L) 𝔄 x" for x
            using Dβ by (auto simp: M_def)
          then have "tp (M (D L) 𝔄 x) < tp (D L)" if "x ∈ A''" for x
            using lless that ‹A'' ⊆ A'› lL by force
          then have [simp]: "{x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)} = {}"
            using leD by blast
          show False
            using α ‹α ≥ ω› by simp
        qed
        then show ?thesis
          by (meson Ord_linear2 Ord_ordertype ‹Ord α›)
      qed
      let ?U = "UNIV :: nat set"
      define μ where "μ ≡ fst ∘ from_nat_into (elts β × ?U)"
      define q where "q ≡ to_nat_on (elts β × ?U)"
      have co_βU: "countable (elts β × ?U)"
        by (simp add: β less_ω1_imp_countable)
      moreover have "elts β × ?U ≠ {}"
        using ‹0 ∈ elts β› by blast
      ultimately have "range (from_nat_into (elts β × ?U)) = (elts β × ?U)"
        by (metis range_from_nat_into)
      then have μ_in_β [simp]: "μ i ∈ elts β" for i
        by (metis SigmaE μ_def comp_apply fst_conv range_eqI)

      then have Ord_μ [simp]: "Ord (μ i)" for i
        using Ord_in_Ord by blast

      have inf_βU: "infinite (elts β × ?U)"
        using ‹0 ∈ elts β› finite_cartesian_productD2 by auto

      have 11 [simp]: "μ (q (ν,n)) = ν" if "ν ∈ elts β" for ν n
        by (simp add: μ_def q_def that co_βU)
      have range_μ [simp]: "range μ = elts β"
        by (auto simp: image_iff) (metis 11)
      have [simp]: "KI i {} = UNIV" "KI i (insert a X) = K i a ∩ KI i X" for i a X
        by (auto simp: KI_def)
      define Φ where "Φ ≡ λn::nat. λ𝔄 x. (∀ν ∈ elts β. 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α)
                                        ∧ x ` {..<n} ⊆ elts (α*β)
                                        ∧ (⋃ν ∈ elts β. 𝔄 ν) ⊆ KI 1 (x ` {..<n}) 
                                        ∧ strict_mono_sets (elts β) 𝔄"
      define Ψ where "Ψ ≡ λn::nat. λg 𝔄 𝔄' xn. g ∈ elts β → elts β ∧ strict_mono_on (elts β) g
                  ∧ (∀i≤n. g (μ i) = μ i)
                  ∧ (∀ν ∈ elts β. 𝔄' ν ⊆ K 1 xn ∩ 𝔄 (g ν))
                  ∧ {xn} ≪ (𝔄' (μ n)) ∧ xn ∈ 𝔄 (μ n)"
      let ?𝔄0 = "λν. plus (α * ν) ` elts α"
      have base: "Φ 0 ?𝔄0 x" for x
        by (auto simp: Φ_def add_mult_less add_mult_less_add_mult ordertype_image_plus strict_mono_sets_def less_sets_def)
      have step: "Ex (λ(g,𝔄',xn). Ψ n g 𝔄 𝔄' xn ∧ Φ (Suc n) 𝔄' (x(n:=xn)))" if "Φ n 𝔄 x" for n 𝔄 x
      proof -
        have 𝔄: "⋀ν. ν ∈ elts β ⟹ 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α"
          and x: "x ` {..<n} ⊆ elts (α*β)"
          and sub: "⋃ (𝔄 ` elts β) ⊆ KI (Suc 0) (x ` {..<n})"
          and sm: "strict_mono_sets (elts β) 𝔄"
          and μβ: "μ ` {..n} ⊆ elts β" and 𝔄sub: "𝔄 (μ n) ⊆ elts (α*β)"
          and 𝔄fun: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}"
          using that by (auto simp: Φ_def)
        then obtain xn g where xn: "xn ∈ 𝔄 (μ n)" and g: "g ∈ elts β → elts β"
          and sm_g: "strict_mono_on (elts β) g" and g_μ: "∀ν ∈ μ`{..n}. g ν = ν"
          and g_α: "∀ν ∈ elts β. α ≤ tp (K 1 xn ∩ 𝔄 (g ν))"
          using 10 [OF _ μβ 𝔄sub _ 𝔄fun] by (auto simp: 𝔄)
        have tp1: "tp (K 1 xn ∩ 𝔄 (g ν)) = α" if "ν ∈ elts β" for ν
          by (metis antisym Int_lower2 PiE 𝔄 down g g_α ordertype_VWF_mono that)
        have tp2: "tp (𝔄 (μ n)) = α"
          by (auto simp: 𝔄)
        obtain "small (𝔄 (μ n))" "𝔄 (μ n) ⊆ ON"
          by (meson 𝔄sub ord down elts_subset_ON subset_trans)
        then obtain A2 where A2: "tp A2 = α" "A2 ⊆ K 1 xn ∩ 𝔄 (μ n)" "{xn} ≪ A2"
          using indecomposable_imp_Ex_less_sets [OF indec ‹α ≥ ω› tp2]
          by (metis μ_in_β atMost_iff image_eqI inf_le2 le_refl xn tp1 g_μ)
        then have A2_sub: "A2 ⊆ 𝔄 (μ n)" by simp
        let ?𝔄 = "λν. if ν = μ n then A2 else K 1 xn ∩ 𝔄 (g ν)"
        have [simp]: "({..<Suc n} ∩ {x. x ≠ n}) = ({..<n})"
          by auto
        have "K (Suc 0) xn ∩ (⋃x∈elts β ∩ {ν. ν ≠ μ n}. 𝔄 (g x)) ⊆ KI (Suc 0) (x ` {..<n})"
          using sub g by (auto simp: KI_def)
        moreover have "A2 ⊆ KI (Suc 0) (x ` {..<n})" "A2 ⊆ elts (α*β)" "xn ∈ elts (α*β)"
          using 𝔄sub sub A2 xn by fastforce+
        moreover have "strict_mono_sets (elts β) ?𝔄"
          using sm sm_g g g_μ A2_sub
          unfolding strict_mono_sets_def strict_mono_on_def less_sets_def Pi_iff subset_iff Ball_def Bex_def image_iff
          by (simp (no_asm_use) add: if_split_mem2) (smt order_refl)
        ultimately have "Φ (Suc n) ?𝔄 (x(n := xn))"
          using tp1 x A2 by (auto simp: Φ_def K_def)
        with A2 show ?thesis
          by (rule_tac x="(g,?𝔄,xn)" in exI) (simp add: Ψ_def g sm_g g_μ xn)
      qed
      define G where "G ≡ λn 𝔄 x. @(g,𝔄',x'). ∃xn. Ψ n g 𝔄 𝔄' xn ∧ x' = (x(n:=xn)) ∧ Φ (Suc n) 𝔄' x'"
      have GΦ: "(λ(g,𝔄',x'). Φ (Suc n) 𝔄' x') (G n 𝔄 x)"
        and GΨ: "(λ(g,𝔄',x'). Ψ n g 𝔄 𝔄' (x' n)) (G n 𝔄 x)"  if "Φ n 𝔄 x" for n 𝔄 x
        using step [OF that] by (force simp: G_def dest: some_eq_imp)+
      define H where "H ≡ rec_nat (id,?𝔄0,undefined) (λn (g0,𝔄,x0). G n 𝔄 x0)"
      have "(λ(g,𝔄,x). Φ n 𝔄 x) (H n)" for n
        unfolding H_def by (induction n) (use GΦ base in fastforce)+
      then have H_imp_Φ: "Φ n 𝔄 x" if "H n = (g,𝔄,x)" for g 𝔄 x n
        by (metis case_prodD that)
      then have H_imp_Ψ: "(λ(g,𝔄',x'). let (g0,𝔄,x) = H n in Ψ n g 𝔄 𝔄' (x' n)) (H (Suc n))" for n
        using GΨ by (fastforce simp: H_def split: prod.split)
      define g where "g ≡ λn. (λ(g,𝔄,x). g) (H (Suc n))"
      have g: "g n ∈ elts β → elts β" and sm_g: "strict_mono_on (elts β) (g n)"
        and 13: "⋀i. i≤n ⟹ g n (μ i) = μ i" for n
        using H_imp_Ψ [of n] by (auto simp: g_def Ψ_def)
      define 𝔄 where "𝔄 ≡ λn. (λ(g,𝔄,x). 𝔄) (H n)"
      define x where "x ≡ λn. (λ(g,𝔄,x). x n) (H (Suc n))"
      have 14: "𝔄 (Suc n) ν ⊆ K 1 (x n) ∩ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n
        using H_imp_Ψ [of n] that by (force simp: Ψ_def 𝔄_def x_def g_def)
      then have x14: "𝔄 (Suc n) ν ⊆ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n
        using that by blast
      have 15: "x n ∈ 𝔄 n (μ n)" and 16: "{x n} ≪ (𝔄 (Suc n) (μ n))" for n
        using H_imp_Ψ [of n] by (force simp: Ψ_def 𝔄_def x_def)+
      have 𝔄_αβ: "𝔄 n ν ⊆ elts (α*β)" if "ν ∈ elts β" for ν n
        using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
      have 12: "strict_mono_sets (elts β) (𝔄 n)" for n
        using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
      let ?Z = "range x"
      have S_dec: "⋃ (𝔄 (m+k) ` elts β) ⊆ ⋃ (𝔄 m ` elts β)" for k m
        by (induction k) (use 14 g in ‹fastforce+›)
      have "x n ∈ K 1 (x m)" if "m<n" for m n
      proof -
        have "x n ∈ (⋃ν ∈ elts β. 𝔄 n ν)"
          by (meson "15" UN_I μ_in_β)
        also have "… ⊆ (⋃ν ∈ elts β. 𝔄 (Suc m) ν)"
          using S_dec [of "Suc m"] less_iff_Suc_add that by auto
        also have "… ⊆ K 1 (x m)"
          using 14 by auto
        finally show ?thesis .
      qed
      then have "f{x m, x n} = 1" if "m<n" for m n
        using that by (auto simp: K_def)
      then have Z_K1: "f ` [?Z]⇗2⇖ ⊆ {1}"
        by (clarsimp simp: nsets_2_eq) (metis insert_commute less_linear)
      moreover have Z_sub: "?Z ⊆ elts (α*β)"
        using "15" 𝔄_αβ μ_in_β by blast
      moreover have "tp ?Z ≥ ω * β"
      proof -
        define 𝔤 where "𝔤 ≡ λi j x. wfrec (measure (λk. j-k)) (λ𝔤 k. if k<j then g k (𝔤 (Suc k)) else x) i"
        have 𝔤: "𝔤 i j x = (if i<j then g i (𝔤 (Suc i) j x) else x)" for i j x
          by (simp add: 𝔤_def wfrec cut_apply)
        have 17: "𝔤 k j (μ i) = μ i" if "i ≤ k" for i j k
          using wf_measure [of "λk. j-k"] that
          by (induction k rule: wf_induct_rule) (simp add: "13" 𝔤 le_imp_less_Suc)
        have 𝔤_in_β: "𝔤 i j ν  ∈ elts β" if "ν ∈ elts β" for i j ν
          using wf_measure [of "λk. j-k"] that
        proof (induction i rule: wf_induct_rule)
          case (less i)
          with g show ?case by (force simp: 𝔤 [of i])
        qed
        then have 𝔤_fun: "𝔤 i j ∈ elts β → elts β" for i j
          by simp
        have sm_𝔤: "strict_mono_on (elts β) (𝔤 i j)" for i j
          using wf_measure [of "λk. j-k"]
        proof (induction i rule: wf_induct_rule)
          case (less i)
          with sm_g show ?case
            by (auto simp: 𝔤 [of i] strict_mono_on_def 𝔤_in_β)
        qed
        have *: "𝔄 j (μ j) ⊆ 𝔄 i (𝔤 i j (μ j))" if "i < j" for i j
          using wf_measure [of "λk. j-k"] that
        proof (induction i rule: wf_induct_rule)
          case (less i)
          then have "j - Suc i < j - i"
            by (metis (no_types) Suc_diff_Suc lessI)
          with less 𝔤_in_β show ?case
            by (simp add: 𝔤 [of i]) (metis 17 Suc_lessI μ_in_β order_refl order_trans x14)
        qed
        have le_iff: "𝔤 i j (μ j) ≤ μ i ⟷ μ j ≤ μ i" for i j
          using sm_𝔤 unfolding strict_mono_on_def
          by (metis "17" Ord_in_Ord Ord_linear2 μ_in_β leD le_refl less_V_def ‹Ord β›)
        then have less_iff: "𝔤 i j (μ j) < μ i ⟷ μ j < μ i" for i j
          by (metis (no_types, lifting) "17" μ_in_β less_V_def order_refl sm_𝔤 strict_mono_on_def)
        have eq_iff: "𝔤 i j (μ j) = μ i ⟷ μ j = μ i" for i j
          by (metis eq_refl le_iff less_iff less_le)
        have μ_if_ne: "μ m < μ n" if mn: "𝔄 m (μ m) ≪ 𝔄 n (μ n)" "m ≠ n" for m n
        proof -
          have xmn: "x m < x n"
            using "15" less_setsD that(1) by blast
          have Ord𝔤: "Ord (𝔤 n m (μ m))"
            using Ord_in_Ord 𝔤_in_β μ_in_β ord(2) by presburger
          have "¬ 𝔄 m (μ m) ≪ 𝔄 n (μ n)" if "μ n = μ m"
            using  "*" "15" eq_iff that unfolding less_sets_def
            by (metis in_mono less_irrefl not_less_iff_gr_or_eq)
          moreover
          have "𝔄 n (μ n) ⊆ 𝔄 m (𝔤 m n (μ n)) ∨ 𝔄 m (μ m) ⊆ 𝔄 n (𝔤 n m (μ m))"
            using * mn
            by (meson antisym_conv3)
          then have False if "μ n < μ m"
            using strict_mono_setsD [OF 12] 15 xmn 𝔤_in_β μ_in_β that
            by (smt (verit, best) Ord𝔤 Ord_μ Ord_linear2 leD le_iff less_asym less_iff less_setsD subset_iff)
          ultimately show "μ m < μ n"
            by (meson that(1) Ord_μ Ord_linear_lt)
        qed
        have 18: "𝔄 m (μ m) ≪ 𝔄 n (μ n) ⟷ μ m < μ n" for m n
        proof (cases n m rule: linorder_cases)
          case less
          show ?thesis
          proof (intro iffI)
            assume "μ m < μ n"
            then have "𝔄 n (𝔤 n m (μ m)) ≪ 𝔄 n (μ n)"
              by (metis "12" 𝔤_in_β μ_in_β eq_iff le_iff less_V_def strict_mono_sets_def)
            then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)"
              by (meson "*" less less_sets_weaken1)
          qed (use μ_if_ne less in blast)
        next
          case equal
          with 15 show ?thesis by auto
        next
          case greater
          show ?thesis
          proof (intro iffI)
            assume "μ m < μ n"
            then have "𝔄 m (μ m) ≪ (𝔄 m (𝔤 m n (μ n)))"
              by (meson 12 Ord_in_Ord Ord_linear2 𝔤_in_β μ_in_β le_iff leD ord(2) strict_mono_sets_def)
            then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)"
              by (meson "*" greater less_sets_weaken2)
          qed (use μ_if_ne greater in blast)
        qed
        have 𝔄_increasing_μ: "𝔄 n (μ n) ⊆ 𝔄 m (μ m)" if "m ≤ n" "μ m = μ n" for m n
          by (metis "*" "17" dual_order.order_iff_strict that)
        moreover have INF: "infinite {n. n ≥ m ∧ μ m = μ n}" for m
        proof -
          have "infinite (range (λn. q (μ m, n)))"
            unfolding q_def
            using to_nat_on_infinite [OF co_βU inf_βU] finite_image_iff
            by (simp add: finite_image_iff inj_on_def)
          moreover have "(range (λn. q (μ m, n))) ⊆ {n. μ m = μ n}"
            using 11 [of "μ m"] by auto
          ultimately have "infinite {n. μ m = μ n}"
            using finite_subset by auto
          then have "infinite ({n. μ m = μ n} - {..<m})"
            by simp
          then show ?thesis
            by (auto simp: finite_nat_set_iff_bounded Bex_def not_less)
        qed
        let ?eqv = "λm. {n. m ≤ n ∧ μ m = μ n}"
        have sm_x: "strict_mono_on (?eqv m) x" for m
        proof (clarsimp simp: strict_mono_on_def)
          fix n p
          assume "m ≤ n" "μ p = μ n" "μ m = μ n" "n < p"
          with 16 [of n] show "x n < x p"
            by (metis "*" "15" "17" Suc_lessI insert_absorb insert_subset le_SucI less_sets_singleton1)
        qed
        then have inj_x: "inj_on x (?eqv m)" for m
          using strict_mono_on_imp_inj_on by blast
        define ZA where "ZA ≡ λm. ?Z ∩ 𝔄 m (μ m)"
        have small_ZA [simp]: "small (ZA m)" for m
          by (metis ZA_def inf_le1 small_image_nat smaller_than_small)
        have 19: "tp (ZA m) ≥ ω" for m
        proof -
          have "x ` {n. m ≤ n ∧ μ m = μ n} ⊆ ZA m"
            unfolding ZA_def using "15" 𝔄_increasing_μ by blast
          then have "infinite (ZA m)"
            using INF [of m] finite_image_iff [OF inj_x] by (meson finite_subset)
          then show ?thesis
            by (simp add: ordertype_infinite_ge_ω)
        qed
        have "∃f ∈ elts ω → ZA m. strict_mono_on (elts ω) f" for m
        proof -
          obtain Z where "Z ⊆ ZA m" "tp Z = ω"
            by (meson 19 Ord_ω le_ordertype_obtains_subset small_ZA)
          moreover have "ZA m ⊆ ON"
            using Ord_in_Ord 𝔄_αβ μ_in_β unfolding ZA_def by blast
          ultimately show ?thesis
            by (metis strict_mono_on_ordertype Pi_mono small_ZA smaller_than_small subset_iff)
        qed
        then obtain φ where φ: "⋀m. φ m ∈ elts ω → ZA m"
          and sm_φ: "⋀m. strict_mono_on (elts ω) (φ m)"
          by metis
        have "Ex(λ(m,ν). ν ∈ elts β ∧ γ = ω * ν + ord_of_nat m)" if "γ ∈ elts (ω * β)" for γ
          using that by (auto simp: mult [of ω β] lift_def elts_ω)
        then obtain split where split: "⋀γ. γ ∈ elts (ω * β) ⟹
             (λ(m,ν). ν ∈ elts β ∧ γ = ω * ν + ord_of_nat m)(split γ)"
          by meson
        have split_eq [simp]: "split (ω * ν + ord_of_nat m) = (m,ν)" if "ν ∈ elts β" for ν m
        proof -
          have [simp]: "ω * ν + ord_of_nat m = ω * ξ + ord_of_nat n ⟷ ξ = ν ∧ n = m" if "ξ ∈ elts β" for ξ n
            by (metis Ord_ω that Ord_mem_iff_less_TC mult_cancellation_lemma ord_of_nat_ω ord_of_nat_inject)
          show ?thesis
            using split [of "ω*ν + m"] that by (auto simp: mult [of ω β] lift_def cong: conj_cong)
        qed
        define π where "π ≡ λγ. (λ(m,ν). φ (q(ν,0)) m)(split γ)"
        have π_Pi: "π ∈ elts (ω * β) → (⋃m. ZA m)"
          using φ by (fastforce simp: π_def mult [of ω β] lift_def elts_ω)
        moreover have "(⋃m. ZA m) ⊆ ON"
          unfolding ZA_def using 𝔄_αβ μ_in_β elts_subset_ON by blast
        ultimately have Ord_π_Pi: "π ∈ elts (ω * β) → ON"
          by fastforce
        show "tp ?Z ≥ ω * β"
        proof -
          have †: "(⋃m. ZA m) = ?Z"
            using "15" by (force simp: ZA_def)
          moreover
          have "tp (elts (ω * β)) ≤ tp (⋃m. ZA m)"
          proof (rule ordertype_inc_le)
            show "π ` elts (ω * β) ⊆ (⋃m. ZA m)"
              using π_Pi by blast
          next
            fix u v
            assume x: "u ∈ elts (ω * β)" and y: "v ∈ elts (ω * β)" and "(u,v) ∈ VWF"
            then have "u<v"
              by (meson Ord_ω Ord_in_Ord Ord_mult VWF_iff_Ord_less ord(2))
            moreover
            obtain m ν n ξ where ueq: "u = ω * ν + ord_of_nat m" and ν: "ν ∈ elts β"
              and veq: "v = ω * ξ + ord_of_nat n" and ξ: "ξ ∈ elts β"
              using x y by (auto simp:  mult [of ω β] lift_def elts_ω)
            ultimately have "ν ≤ ξ"
              by (meson Ord_ω Ord_in_Ord Ord_linear2 ‹Ord β› add_mult_less_add_mult less_asym ord_of_nat_ω)
            consider (eq) "ν = ξ" | (lt) "ν < ξ"
              using ‹ν ≤ ξ› le_neq_trans by blast
            then have "π u < π v"
            proof cases
              case eq
              then have "m < n"
                using ueq veq ‹u<v› by simp
              then have "φ (q (ξ, 0)) m < φ (q (ξ, 0)) n"
                using sm_φ strict_mono_onD by blast
              then show ?thesis
                using eq ueq veq ν ‹m < n› by (simp add: π_def)
            next
              case lt
              have "φ (q(ν,0)) m ∈ 𝔄 (q(ν,0)) (μ(q(ν,0)))" "φ (q (ξ,0)) n ∈ 𝔄 (q(ξ,0)) (μ(q(ξ,0)))"
                using φ unfolding ZA_def by blast+
              then show ?thesis
                using lt ueq veq ν ξ 18 [of "q(ν,0)" "q(ξ,0)"]
                by (simp add: π_def less_sets_def)
            qed
            then show "(π u, π v) ∈ VWF"
              using π_Pi by (metis Ord_π_Pi PiE VWF_iff_Ord_less x y mem_Collect_eq)
          qed (use † in auto)
          ultimately show ?thesis by simp
        qed
      qed
      then obtain Z where "Z ⊆ ?Z" "tp Z = ω * β"
        by (meson Ord_ω Ord_mult ord Z_sub down le_ordertype_obtains_subset)
      ultimately show False
        using iii [of Z] by (meson dual_order.trans image_mono nsets_mono)
    qed
    have False
      if 0: "∀H. tp H = ord_of_nat (2*k) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {0}"
        and 1: "∀H. tp H = min γ (ω * β) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}"
    proof (cases "ω*β ≤ γ")
      case True
      then have †: "∃H'⊆H. tp H' = ω * β" if "tp H = γ" "small H" for H
        by (metis Ord_ω Ord_ω1 Ord_in_Ord Ord_mult β le_ordertype_obtains_subset that)
      have [simp]: "min γ (ω*β) = ω*β"
        by (simp add: min_absorb2 that True)
      then show ?thesis
        using * [OF 0] 1 True
        by simp (meson † down image_mono nsets_mono subset_trans)
    next
      case False
      then have †: "∃H'⊆H. tp H' = γ" if "tp H = ω * β" "small H" for H
        by (metis Ord_linear_le Ord_ordertype ‹Ord γ› le_ordertype_obtains_subset that)
      then have "γ ≤ ω*β"
        by (meson Ord_ω Ord_ω1 Ord_in_Ord Ord_linear_le Ord_mult β ‹Ord γ› False)
      then have [simp]: "min γ (ω*β) = γ"
        by (simp add: min_absorb1)
      then show ?thesis
        using * [OF 0] 1 False
        by simp (meson † down image_mono nsets_mono subset_trans)
    qed
    then show "∃i<Suc (Suc 0). ∃H⊆elts (α*β). tp H = [ord_of_nat (2*k), min γ (ω*β)] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}"
      by force
  qed
qed


theorem Erdos_Milner:
  assumes ν: "ν ∈ elts ω1"
  shows "partn_lst_VWF (ω↑(1 + ν * n)) [ord_of_nat (2^n), ω↑(1+ν)] 2"
proof (induction n)
  case 0
  then show ?case
    using partn_lst_VWF_degenerate [of 1 2] by simp
next
  case (Suc n)
  have "Ord ν"
    using Ord_ω1 Ord_in_Ord assms by blast
  have "1+ν ≤ ν+1"
    by (simp add: ‹Ord ν› one_V_def plus_Ord_le)
  then have [simp]: "min (ω ↑ (1 + ν)) (ω * ω ↑ ν) = ω ↑ (1+ν)"
    by (simp add: ‹Ord ν› oexp_add min_def)
  have ind: "indecomposable (ω ↑ (1 + ν * ord_of_nat n))"
    by (simp add: ‹Ord ν› indecomposable_ω_power)
  show ?case
  proof (cases "n = 0")
    case True
    then show ?thesis
      using partn_lst_VWF_ω_2 ‹Ord ν› one_V_def by auto
  next
    case False
    then have "Suc 0 < 2 ^ n"
      using less_2_cases not_less_eq by fastforce
    then have "partn_lst_VWF (ω ↑ (1 + ν * n) * ω ↑ ν) [ord_of_nat (2 * 2 ^ n), ω ↑ (1 + ν)] 2"
      using Erdos_Milner_aux [OF Suc ind, where β = "ω↑ν"] ‹Ord ν› ν
      by (auto simp: countable_oexp)
    then show ?thesis
      using ‹Ord ν› by (simp add: mult_succ mult.assoc oexp_add)
  qed
qed


corollary remark_3: "partn_lst_VWF (ω↑(Suc(4*k))) [4, ω↑(Suc(2*k))] 2"
  using Erdos_Milner [of "2*k" 2] 
  apply (simp flip: ord_of_nat_mult ord_of_nat.simps)
  by (simp add: one_V_def)


text ‹Theorem 3.2 of Jean A. Larson, ibid.›
corollary Theorem_3_2:
  fixes k n::nat
  shows "partn_lst_VWF (ω↑(n*k)) [ω↑n, ord_of_nat k] 2"
proof (cases "n=0 ∨ k=0")
  case True
  then show ?thesis
    by (auto intro: partn_lst_triv0 [where i=1] partn_lst_triv1 [where i=0])
next
  case False
  then have "n > 0" "k > 0"
    by auto
  from ‹k > 0› less_exp [of ‹k - 1›] have ‹k ≤ 2 ^ (k - 1)›
    by (cases k) (simp_all add: less_eq_Suc_le)
  have PV: "partn_lst_VWF (ω ↑ (1 + ord_of_nat (n-1) * ord_of_nat (k-1))) [ord_of_nat (2 ^ (k-1)), ω ↑ (1 + ord_of_nat (n-1))] 2"
    using Erdos_Milner [of "ord_of_nat (n-1)" "k-1"] Ord_ω1 Ord_mem_iff_lt less_imp_le by blast
  have "k+n ≤ Suc (k * n)"
    using False not0_implies_Suc by fastforce
  then have "1 + (n - 1) * (k - 1) ≤ n*k"
    using False by (auto simp: algebra_simps)
  then have "(1 + ord_of_nat (n - 1) * ord_of_nat (k - 1)) ≤ ord_of_nat(n*k)"
    by (metis (mono_tags, lifting) One_nat_def one_V_def ord_of_nat.simps ord_of_nat_add ord_of_nat_mono_iff ord_of_nat_mult)
  then have x: "ω ↑ (1 + ord_of_nat (n - 1) * ord_of_nat (k - 1)) ≤ ω↑(n*k)"
    by (simp add: oexp_mono_le)
  then have "partn_lst_VWF (ω↑(n*k)) [ω ↑ (1 + ord_of_nat (n-1)), ord_of_nat (2 ^ (k-1))] 2"
    by (metis PV partn_lst_two_swap Partitions.partn_lst_greater_resource less_eq_V_def)
  then have "partn_lst_VWF (ω↑(n*k)) [ω ↑ n, ord_of_nat (2 ^ (k-1))] 2"
    using ord_of_minus_1 [OF ‹n > 0›] by (simp add: one_V_def)
  then show ?thesis
    using ‹k ≤ 2 ^ (k - 1)›
    by (auto elim!: partn_lst_less simp add: less_Suc_eq)
qed

end