Try skirting axiom of choice

Author: nguyenvukhang

Munkres/Mathlib/MonotoneSubseq.lean

@@ -3,9 +3,15 @@ import Munkres.Mathlib.Prelude
 
 open Set Filter Topology TopologicalSpace
 
-variable {x : ℕ → ℝ}
+universe u
 
-private def IsPeak (x : ℕ → ℝ) (n : ℕ) := ∀ m ≥ n, x m ≤ x n
+variable {α : Type u} [Preorder α]
+  {x : ℕ → ℝ}
+
+private def IsPeak₂ (x : ℕ → ℝ) (n : ℕ) : Prop := Minimal (· ∈ Set.range x) n
+noncomputable example : DecidablePred fun n ↦ IsPeak₂ x n := by
+  exact Classical.decPred fun n ↦ IsPeak₂ x n
+private def IsPeak (x : ℕ → ℝ) (n : ℕ) : Prop := ∀ m ≥ n, x m ≤ x n
 
 private lemma p' {n : ℕ} (h : ¬IsPeak x n) : ∃ m > n, x m > x n
   := by --
@@ -18,20 +24,88 @@ private lemma p' {n : ℕ} (h : ¬IsPeak x n) : ∃ m > n, x m > x n
     exact (lt_self_iff_false (x m)).mp hlt
   exact ⟨m, hmn.lt_of_ne' this, hlt⟩ -- ∎
 
-private structure Node (x : ℕ → ℝ) (N : ℕ) where
+private structure Node (N : ℕ) where
   n : ℕ
   ge' : n ≥ N
 
 private noncomputable def ζ {x : ℕ → ℝ} {N : ℕ}
-  (h : ∀ n ≥ N, ∃ m > n, x m > x n) : ℕ → Node x N
+  (h : ∀ n ≥ N, ∃ m > n, x m > x n) : ℕ → Node N
   | 0 => { n := N, ge' := le_rfl }
   | n + 1 => by
     let p := ζ h n
-    let m := (h p.n p.ge').choose
-    have hm := (h p.n p.ge').choose_spec.1
+    have : DecidablePred fun m ↦ m > n ∧ x m > x n := by
+      sorry
+    let m := Nat.find <| h p.n p.ge'
+    have hm := (Nat.find_spec (h p.n p.ge')).1
     exact { n := m, ge' := p.ge'.trans hm.le }
 
-noncomputable example {x : ℕ → ℝ}
+private structure Node₂ (x : ℕ → ℝ) where
+  n : ℕ
+  peak' : IsPeak x n
+
+
+private noncomputable def ψ {x : ℕ → ℝ}
+  (h : ∀ N, ∃ n > N, IsPeak x n) : ℕ → Node₂ x
+  | 0 => by
+    specialize h 0
+    exact { n := h.choose, peak' := h.choose_spec.2 }
+  | n + 1 => by
+    let p := ψ h n
+    specialize h p.n
+    exact { n := h.choose, peak' := h.choose_spec.2 }
+
+
+example {x : Fin 0} : False := by
+  have : x.val < 0 := x.prop
+  exact Nat.not_succ_le_zero (↑x) this
+
+private lemma l₁ {α : Type u} [Preorder α] [h₀ : Inhabited α] {A : Set α}
+  (hA : A.Finite) : (upperBounds A).Nonempty := by
+  have : Finite A := hA
+  rw [finite_iff_exists_equiv_fin] at this
+  obtain ⟨n, φ, ψ, h₁, h₂⟩ := this
+  induction n with
+  | zero =>
+    use h₀.default
+    intro x hx
+    let φ : A ≃ Fin 0 := { toFun := φ, invFun := ψ, left_inv := h₁, right_inv := h₂ }
+    let n := φ ⟨x, hx⟩
+    refine False.elim <| Nat.not_succ_le_zero n n.prop
+  | succ n ih =>
+    sorry
+#print axioms l₁
+
+private lemma mono {x : ℕ → α} (hPf : (Set.range x).Finite)
+  : ∃ φ : ℕ → ℕ, StrictMono φ ∧ Monotone (x ∘ φ)
+  := by
+  let P := Set.range x
+  -- have : P.Finite := hPf
+  -- let P' := hPf.toFinset
+  have : ∃ N, ∀ n ∈ P, n < N := by
+    -- if hP : P = ∅ then
+    --   sorry
+    -- else
+    sorry
+    -- if hP₀ : P'.Nonempty then
+    --   use P'.max' hP₀ + 1
+    --   intro n hn
+    --   rw [<-hPf.mem_toFinset] at hn
+    --   -- rw [Order.lt_add_one_iff]
+    --   -- exact P'.le_max' n hn
+    --   sorry
+    -- else
+    -- have hP₀ : P = ∅ := by
+    --   have : P' = ∅ := Finset.not_nonempty_iff_eq_empty.mp hP₀
+    --   exact Finite.toFinset_eq_empty.mp this
+    -- use 0
+    -- intro n hn
+    -- rw [hP₀] at hn
+    -- exact False.elim hn
+  -- obtain ⟨N, hN⟩ := this
+  sorry
+-- #print axioms mono
+
+private lemma both {x : ℕ → ℝ}
   : ∃ φ : ℕ → ℕ, StrictMono φ ∧ (Monotone (x ∘ φ) ∨ Antitone (x ∘ φ))
   := by
   let P := { n | IsPeak x n }
@@ -66,23 +140,41 @@ noncomputable example {x : ℕ → ℝ}
       intro n
       let p := ζ hδ n
       specialize hδ (φ n) p.ge'
-      exact hδ.choose_spec.1
+      exact (Nat.find_spec hδ).1
     · refine monotone_nat_of_le_succ ?_
       intro n
       let p := ζ hδ n
       specialize hδ (φ n) p.ge'
-      exact hδ.choose_spec.2.le
+      exact (Nat.find_spec hδ).2.le
   else
-  have : ∀ N, ∃ n ≥ N, IsPeak x n := by
+  have h : ∀ N, ∃ n > N, IsPeak x n := by
     intro N
     by_contra! h
-    have h : P ⊆ Finset.range N := by
+    let R := Finset.range (N + 1)
+    have h : P ⊆ R := by
       rw [Finset.coe_range]
       intro n hnP
       by_contra! hn
       rw [notMem_Iio] at hn
       exact (h n hn) hnP
-    have : (SetLike.coe <| Finset.range N).Finite := (Finset.range N).finite_toSet
+    have : (SetLike.coe R).Finite := R.finite_toSet
     have : P.Finite := this.subset h
     exact hPf this
-  sorry
+  let φ (n : ℕ) : ℕ := (ψ h n).n
+  refine ⟨φ, ?_, Or.inr ?_⟩
+  · refine strictMono_nat_of_lt_succ ?_
+    intro n
+    let p := ψ h n
+    exact (h p.n).choose_spec.1
+  · refine antitone_nat_of_succ_le ?_
+    intro n
+    let p := ψ h n
+    simp only [Function.comp_apply]
+    have hp : IsPeak x (φ n) := by
+      match n with
+      | 0 => exact (h 0).choose_spec.2
+      | n + 1 => exact (h (ψ h n).n).choose_spec.2
+    have : φ n < φ (n + 1) := (h p.n).choose_spec.1
+    exact hp (φ (n + 1)) this.le
+
+-- #print axioms mono