Clean up

Author: nguyenvukhang

Makefile

@@ -14,6 +14,7 @@ check: generate
 generate:
 	slope generate Rudin.Alpha
 	slope generate Rudin.Partition
+	slope generate Rudin.Partition.Prelude
 	slope generate Rudin.Prelude
 	slope generate Rudin.Lemmas
 

Rudin/Partition.lean

@@ -12,8 +12,8 @@ import Rudin.Partition.Interval
 import Rudin.Partition.Monotone
 import Rudin.Partition.OrderBot
 import Rudin.Partition.Prelude
-import Rudin.Partition.Prelude.Nodup
-import Rudin.Partition.Prelude.SortedList
+import Rudin.Partition.Prelude.OrderedInsert
+import Rudin.Partition.Prelude.SortedLE
 import Rudin.Partition.Single
 import Rudin.Partition.SpecialPartitions
 import Rudin.Partition.Union

Rudin/Partition/Insert.lean

@@ -38,10 +38,9 @@ noncomputable def ι (h : IsInsertable x P) : Partition I
   := by --
   let l' := P.l.orderedInsert (· ≤ ·) x
   have sorted' : l'.SortedLT := by
-    sorry
-    -- refine P.sorted'.orderedInsert_sorted_lt ?_
-    -- rw [<-P.mem_iff_mem_list]
-    -- exact h.notMem'
+    refine P.sorted'.orderedInsert_sorted_lt ?_
+    rw [<-P.mem_iff_mem_list]
+    exact h.notMem'
   have h₀ : l' ≠ [] := by
     refine List.ne_nil_of_length_pos ?_
     rw [List.orderedInsert_length]
@@ -53,7 +52,7 @@ noncomputable def ι (h : IsInsertable x P) : Partition I
       have ha' : a ∈ l' := by
         rw [List.mem_orderedInsert]
         exact Or.inr P.mem_aᵢ
-      exact List.sorted_head_min h₀ sorted'.sortedLE a ha'
+      exact sorted'.sortedLE.sorted_head_min h₀ a ha'
     · -- a ≤ head. This follows from the minimality of a ∈ P.
       have h : l'.head h₀ ∈ l' := List.head_mem h₀
       rw [List.mem_orderedInsert] at h
@@ -76,7 +75,7 @@ noncomputable def ι (h : IsInsertable x P) : Partition I
       have hb' : b ∈ l' := by
         rw [List.mem_orderedInsert]
         exact Or.inr P.mem_bᵢ
-      exact List.sorted_last_max h₀ sorted'.sortedLE b hb' -- ∎
+      exact sorted'.sortedLE.sorted_last_max h₀ b hb' -- ∎
 
 noncomputable def ι' (x : ℝ) (P : Partition I) : Partition I
   := by --

Rudin/Partition/Prelude.lean

@@ -1,3 +1,5 @@
-import Rudin.Partition.Prelude.Nodup
-import Rudin.Partition.Prelude.SortedList
+import Rudin.Partition.Prelude.OrderedInsert
+import Rudin.Partition.Prelude.SortedLE
+set_option linter.style.longLine false
+
 -- WARNING: THIS FILE IS AUTO-GENERATED.

Rudin/Partition/Prelude/Nodup.lean …din/Partition/Prelude/OrderedInsert.leanRudin/Partition/Prelude/Nodup.lean renamed to Rudin/Partition/Prelude/OrderedInsert.lean Rudin/Partition/Prelude/Nodup.lean renamed to Rudin/Partition/Prelude/OrderedInsert.lean

@@ -38,26 +38,20 @@ theorem Nodup.orderedInsert (hl : l.Nodup) (hx : x ∉ l) : (l.orderedInsert (·
   let r : ℝ → ℝ → Prop := (· ≤ ·)
   induction l with
   | nil =>
-    rw [List.orderedInsert, nodup_cons];
+    rw [List.orderedInsert, nodup_cons]
     exact ⟨not_mem_nil, hl⟩
   | cons y ys ih =>
-    have hys : ys.Nodup := hl.of_cons
-    have hxys : x ∉ ys := not_mem_of_not_mem_cons hx
-    specialize ih hl.of_cons (not_mem_of_not_mem_cons hx)
-    change (ys.orderedInsert r x).Nodup at ih
     change ((y :: ys).orderedInsert r x).Nodup
     rw [List.orderedInsert]
-    if hle : x ≤ y then
-      have : r x y := hle
-      simp only [↓reduceIte, this]
+    if hle : r x y then -- x ≤ y
+      simp only [↓reduceIte, hle]
       exact hl.cons hx
     else
-      have : ¬r x y := hle
-      simp only [↓reduceIte, this]
+      simp only [↓reduceIte, hle]
       refine nodup_cons.mpr ?_
+      specialize ih hl.of_cons (not_mem_of_not_mem_cons hx)
       refine ⟨?_, ih⟩
-      rw [mem_orderedInsert]
-      push_neg
+      rw [mem_orderedInsert, not_or]
       refine ⟨?_, hl.notMem⟩
       exact (ne_of_not_mem_cons hx).symm -- ∎
 

Rudin/Partition/Prelude/SortedLE.lean

@@ -0,0 +1,38 @@
+import Mathlib.Data.List.NodupEquivFin
+
+universe u
+
+variable {α : Type u} [Preorder α] {l : List α}
+
+namespace List
+
+section Endpoints
+variable (h₀ : l ≠ []) (hl : l.SortedLE)
+
+include h₀ hl in
+theorem SortedLE.sorted_head_min : ∀ x ∈ l, l.head h₀ ≤ x
+  := by --
+  induction l with
+  | nil => contradiction
+  | cons a l ih =>
+    intro x hx
+    change a ≤ x
+    replace hl := List.pairwise_cons.mp hl.pairwise
+    replace hx := List.mem_cons.mp hx
+    rcases hx with hxa | hxl
+    · exact ge_of_eq hxa
+    · exact hl.1 x hxl -- ∎
+
+include h₀ hl in
+theorem SortedLE.sorted_last_max : ∀ x ∈ l, x ≤ l.getLast h₀
+  := by --
+  intro x hx
+  rw [mem_iff_get] at hx
+  obtain ⟨i, hi⟩ := hx
+  subst hi
+  rw [getLast_eq_getElem h₀]
+  exact hl <| Nat.le_sub_one_of_lt i.is_lt -- ∎
+
+end Endpoints
+
+end List

Rudin/Partition/Prelude/SortedList.lean

@@ -1,5 +1,5 @@
 import Rudin.Partition.Endpoints
-import Rudin.Partition.Prelude.SortedList
+import Rudin.Partition.Prelude.SortedLE
 
 namespace Rudin
 
@@ -26,7 +26,7 @@ noncomputable instance : Union (Partition I)
     head' := by
       rw [<-List.head_eq_iff_head?_eq_some hl₀]
       refine le_antisymm ?_ ?_
-      · exact List.sorted_head_min hl₀ hl_sort a hl_a
+      · exact hl_sort.sorted_head_min hl₀ a hl_a
       · have h_min : s.min' hs₀ = a := by
           refine (Finset.min'_eq_iff s hs₀ a).mpr ⟨hs_a, fun x hx ↦ ?_⟩
           rcases Finset.mem_union.mp hx with hx₁ | hx₂
@@ -45,7 +45,7 @@ noncomputable instance : Union (Partition I)
             · exact P₂.max_b x hx₂
         rw [<-h_max]
         exact Finset.le_max' s _ (hl_mem.mp (List.getLast_mem hl₀))
-      · exact List.sorted_last_max hl₀ hl_sort b hl_b
+      · exact hl_sort.sorted_last_max hl₀ b hl_b
     sorted' := Finset.sortedLT_sort s
   } -- ∎