Reformat using https://github.com/wvhulle/lean4

Changes

7 changed files (+181/-78)

• CommitGraph.lean
  • @@ -1,3 +1,6 @@
    + import Std.Time + open Std.Time + /- git log --format=%ct | lake exe commitgraph
  • @@ -31,15 +34,14 @@ Sample output:
    2025-10-12 █▓ -/ - import Std.Time - open Std.Time - - instance : LE PlainDate := leOfOrd + instance : LE PlainDate := + leOfOrd def main : IO Unit := do let stdin ← IO.getStdin - let lines := (← stdin.readToEnd).split "\n" |>.toArray |>.filterMap fun x ↦ - (Timestamp.toPlainDateAssumingUTC ∘ Timestamp.ofSecondsSinceUnixEpoch ∘ Second.Offset.ofNat) <$> x.toNat? + let lines := + (← stdin.readToEnd).split "\n" |>.toArray |>.filterMap fun x ↦ + (Timestamp.toPlainDateAssumingUTC ∘ Timestamp.ofSecondsSinceUnixEpoch ∘ Second.Offset.ofNat) <$> x.toNat? let sorted_lines := lines.qsortOrd if h : 0 < sorted_lines.size then let mut daily := #[]
  • @@ -58,9 +60,12 @@ def main : IO Unit := do
    date := sorted_lines[0] for h : cnt in daily do if i % 7 = 0 then - if i > 0 then IO.println "" - IO.print s!"{date} " + if i > 0 then + IO.println "" + IO.print s! "{date} " date := date.addDays 7 - IO.print <| colors[if cnt = 0 then 0 else if cnt < m / 8 then 1 else if cnt < m / 4 then 2 else if cnt < m / 2 then 3 else 4]'(by grind) + IO.print <| + colors[if cnt = 0 then 0 + else if cnt < m / 8 then 1 else if cnt < m / 4 then 2 else if cnt < m / 2 then 3 else 4]'(by grind) i := i + 1 IO.println ""
• Compose.lean
  • @@ -1,24 +1,36 @@
    import Std.Data.HashMap import Lean.Data.Json.Parser - def ofHex a b := let f (x : Char) := x.toNat - (if x.toNat ≤ '9'.toNat then '0'.toNat else 'a'.toNat - 10) + def ofHex a b := + let f (x : Char) := x.toNat - (if x.toNat ≤ '9'.toNat then '0'.toNat else 'a'.toNat - 10) 16 * (f a) + (f b) |> Char.ofNat def main := do - let keysym := (← IO.FS.lines "keysymdef.h") - |>.map (fun l : String ↦ (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩), Substring.Raw.mk l ⟨11⟩ ⟨30⟩ - |>.takeWhile (· ≠ ' ') |>.toString)) - |> Std.HashMap.ofArray + let keysym := + (← IO.FS.lines "keysymdef.h") |>.map + (fun l : String ↦ + (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩), + Substring.Raw.mk l ⟨11⟩ ⟨30⟩ |>.takeWhile (· ≠ ' ') |>.toString)) |> + Std.HashMap.ofArray IO.println "# Generated by https://git.unnamed.website/miscelleaneous/tree/Compose.lean" IO.println "include \"%L\"" - let raw_abbrs ← IO.Process.run { cmd := "curl", args := #["https://raw.githubusercontent.com/vasnesterov/vscode-lean4/refs/heads/master/lean4-unicode-input/src/abbreviations.json"] } + let raw_abbrs ← + IO.Process.run + { cmd := "curl", + args := + #["https://raw.githubusercontent.com/vasnesterov/vscode-lean4/refs/heads/master/lean4-unicode-input/src/abbreviations.json"] } match Lean.Json.parse raw_abbrs with | .ok (.obj abbrs) => for abbr in abbrs do match abbr.2 with | .str s => if !(s.contains '$') then - -- XCompose doesn't like sequences to be prefixes of other sequences, so append enter to the end - IO.println s!"<Multi_key> <{abbr.1.toList.map (keysym.get! ·) |> "> <".intercalate}> <Return> : \"{s.replace "\\" "\\\\"}\"" - | _ => pure () - | _ => IO.println "parse failure" + -- XCompose doesn't like sequences to be prefixes of other sequences, so append enter to the end + + IO.println + s!"<Multi_key> <{(abbr.1.toList.map (keysym.get! ·) |> + "> <".intercalate)}> <Return> : \"{s.replace "\\" "\\\\"}\"" + | _ => + pure () + | _ => + IO.println "parse failure"
• Kadane.lean
  • @@ -1,39 +1,45 @@
    import Std.Tactic.Do import Mathlib.Analysis.Normed.Ring.Lemmas - def kadane (A : Array ℤ) := Id.run do - let mut cur := 0 - let mut ans := 0 - for x in A do - cur := max x (cur + x) - ans := max ans cur - return ans + def kadane (A : Array ℤ) := + Id.run + (do + let mut cur := 0 + let mut ans := 0 + for x in A do + cur := max x (cur + x) + ans := max ans cur + return ans) def is_max_nonempty_suffix (xs : List ℤ) m := (∃ i ≤ xs.length, (xs.drop i).sum = m) ∧ ∀ i < xs.length, (xs.drop i).sum ≤ m def is_max_subarray (xs : List ℤ) m := - 0 ≤ m ∧ (∃ i ≤ xs.length, ∃ j ≤ xs.length, (xs.extract i j).sum = m) ∧ ∀ i ≤ xs.length, ∀ j ≤ xs.length, (xs.extract i j).sum ≤ m + 0 ≤ m ∧ + (∃ i ≤ xs.length, ∃ j ≤ xs.length, (xs.extract i j).sum = m) ∧ + ∀ i ≤ xs.length, ∀ j ≤ xs.length, (xs.extract i j).sum ≤ m - lemma drop_append_sum [AddMonoid α] {xs ys : List α} (hi : i ≤ xs.length) : (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by - simp [List.drop_append_of_le_length hi] + lemma drop_append_sum [AddMonoid α] {xs ys : List α} (hi : i ≤ xs.length) : + (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by simp [List.drop_append_of_le_length hi] - lemma extract_end_drop {xs : List α} (h : j = xs.length) : xs.extract i j = xs.drop i := by - simp [h] + lemma extract_end_drop {xs : List α} (h : j = xs.length) : xs.extract i j = xs.drop i := by simp [h] - lemma extract_in_bounds {xs ys : List α} (hi : i ≤ xs.length) (hj : j ≤ xs.length) : (xs ++ ys).extract i j = xs.extract i j := by - rw [List.extract_eq_drop_take, List.drop_append_of_le_length hi, List.take_append_of_le_length (by grind)] + lemma extract_in_bounds {xs ys : List α} (hi : i ≤ xs.length) (hj : j ≤ xs.length) : + (xs ++ ys).extract i j = xs.extract i j := by + rw [List.extract_eq_take_drop, List.drop_append_of_le_length hi, List.take_append_of_le_length (by grind)] open Std.Do - theorem kadane_correct : is_max_subarray A.toList (kadane A) := by + theorem kadane_correct : is_max_subarray A.toList (kadane A) := + by generalize h : kadane A = x apply Id.of_wp_run_eq h mvcgen invariants · ⇓⟨xs, ans, cur⟩ => ⌜is_max_nonempty_suffix xs.prefix cur ∧ is_max_subarray xs.prefix ans⌝ case vc1.step ih => expose_names - have hcur_1 : is_max_nonempty_suffix (pref ++ [cur]) cur_1 := by + have hcur_1 : is_max_nonempty_suffix (pref ++ [cur]) cur_1 := + by constructor · by_cases cur ≤ b.snd + cur · obtain ⟨i, hi, hsum⟩ := ih.1.1
• Sort.lean
  • @@ -4,37 +4,42 @@ import Mathlib.Data.Nat.Basic
    variable [LinearOrder α] (A : Array α) - def ICan'tBelieveItCanSort := Id.run do - let N := A.size - let mut A := A.toVector - for hi : i in [:N] do - for hj : j in [:N] do - if A[i] < A[j] then - A := A.swap i j - return A.toArray + def ICan'tBelieveItCanSort := + Id.run + (do + let N := A.size + let mut A := A.toVector + for hi : i in [:N]do + for hj : j in [:N]do + if A[i] < A[j] then + A := A.swap i j + return A.toArray) - #guard let A := #[69, 420, 1, 1, 13, 1, 65536] + #guard + let A := #[69, 420, 1, 1, 13, 1, 65536] ICan'tBelieveItCanSort A = A.qsort open Std.Do -- https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/mvcgen.20doesn't.20produce.20any.20invariant.20goals/near/557949517 - theorem perm : ICan'tBelieveItCanSort A |>.Perm A := by + theorem perm : ICan'tBelieveItCanSort A |>.Perm A := + by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen invariants · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ - · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ - with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm] + · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm] - theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by + theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := + by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen <;> expose_names case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝ case inv2 => - exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) - ∧ ∀ i (_ : i < xs.pos), A'[i]'(by grind [List.length_append, xs.property]) ≤ A'[cur]'(by grind)⌝ + exact ⇓⟨xs, A'⟩ => + ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) ∧ + ∀ i (_ : i < xs.pos), A'[i]'(by grind [List.length_append, xs.property]) ≤ A'[cur]'(by grind)⌝ case vc1.step.isTrue => simp [Array.pairwise_iff_getElem] at h_5 ⊢ grind
  • @@ -46,17 +51,19 @@ theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by
    exact (show r.toArray = r.toArray.extract 0 N by grind) ▸ h_1 all_goals grind - theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort A).Perm A - ∧ (ICan'tBelieveItCanSort A).Pairwise (· ≤ ·) := + theorem ICan'tBelieveICanProveItCanSort : + (ICan'tBelieveItCanSort A).Perm A ∧ (ICan'tBelieveItCanSort A).Pairwise (· ≤ ·) := ⟨perm A, sorted A⟩ -- Not sure why this needs so much boilerplate - abbrev le (a b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) + abbrev le (a b : (ℕ × String)) := + a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) instance : LE (ℕ × String) where le := le @[grind] - lemma le_def {a b : (ℕ × String)} : a ≤ b ↔ le a b := .rfl + lemma le_def {a b : (ℕ × String)} : a ≤ b ↔ le a b := + .rfl instance : LinearOrder (ℕ × String) where le_refl := by grind
• Sum.lean
  • @@ -5,34 +5,45 @@ import Mathlib.Tactic.Rify
    open Finset Filter Topology -- Important: b should be in ℝ so that it's real div not nat div - lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : ∑ a ∈ Ico 2 n, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1)) := by + + lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : + ∑ a ∈ Ico 2 n, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1)) := + by have : ∑ a ∈ Ico 2 n, 1 / (b ^ a) = ∑ a ∈ Ico 2 n, (1 / b) ^ a := by simp rw [this, geom_sum_Ico (by grind) hn] field_simp have : b ^ n ≠ 0 := by positivity grind [inv_pow, mul_pow_sub_one] - lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : + ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = + 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := + by calc ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm - _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (n - 1) * (b - 1))) := by + _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (n - 1) * (b - 1))) := + by apply sum_congr rfl exact fun b bico ↦ geom_sum n b h <| Nat.ofNat_le_cast.mpr <| List.left_le_of_mem_range' bico - _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by apply sum_sub_distrib - _ = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + apply sum_sub_distrib + _ = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := + by suffices ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (n - 1) by rw [this] induction h with - | refl => norm_num + | refl => + norm_num + rfl | step h ih => rw [sum_Ico_succ_top h, ih] simp - -- Exponentials grow quickly - lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by - induction h <;> grind [mul_pow_sub_one] + /-- Exponentials grow quickly -/ + lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by induction h <;> grind [mul_pow_sub_one] - -- Another similar lemma - lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by + /-- Another similar lemma -/ + lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := + by by_cases h : 4 < n · have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by induction h
  • @@ -41,13 +52,14 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind apply Nat.mul_le_mul_right (m * (m - 1)) grind - suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by lia + suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by grind have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] rw [this, mul_le_mul_iff_left₀ (by positivity)] grind · interval_cases n <;> decide - theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by + theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := + by rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)] intro ε εpos simp only [true_and, Set.mem_Ici, Set.mem_Ioo]
  • @@ -57,15 +69,21 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    rw [telescope_sum n h₁] constructor · -- Greater than 1 - ε - suffices (∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1)) ∧ 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by grind + + suffices + (∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1)) ∧ + 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε + by grind constructor - · have h₂ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by - rw [← one_div_mul_one_div] + · have h₂ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := + by + rw [← one_div_mul_one_div ((b : ℝ) ^ (n - 1))] have h₃ : 2 ≤ (b : ℝ) := by norm_cast exact (List.left_le_of_mem_range' bico) - have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := div_le_one₀ (by lia) |>.mpr (by lia) - have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by + have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := div_le_one₀ (by grind) |>.mpr (by grind) + have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := + by simp_rw [one_div] exact inv_anti₀ (by norm_num) <| pow_le_pow_left₀ (by norm_num) h₃ (n - 1) grw [h₄, h₅]
  • @@ -75,27 +93,31 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    norm_cast · by_cases 3 / 2 < ε · have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ - have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by lia) |>.mpr (by lia) + have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by grind) |>.mpr (by grind) suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by grind have := exp_larger n h₁ rw [← one_mul (2 ^ (n - 1))] at this exact div_le_div_iff₀ (by norm_num) (by norm_num) |>.mpr (by norm_cast) · have := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) grw [← this] - have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by + have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := + by field_simp grind rw [← lt_sub_iff_add_lt', this] - have h₂ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by + have h₂ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := + by have := exp_larger' n h₁ rify at this grind [Nat.cast_sub] have h₃ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact div_lt_div_iff₀ h₃ (by nlinarith) |>.mpr h₂ · -- Less than 1 - have h₂ b (bico : b ∈ Ico 2 n) : 0 ≤ (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + + have h₂ b (bico : b ∈ Ico 2 n) : 0 ≤ (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := + by rw [one_div_nonneg] have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) - exact mul_nonneg (pow_nonneg (by lia) (n - 1)) (by lia) + exact mul_nonneg (pow_nonneg (by grind) (n - 1)) (by grind) have : 0 < (1 : ℝ) / (n - 1) := by simp [Nat.one_lt_cast.mpr h₁] grind [sum_nonneg h₂]
• lakefile.toml
  • @@ -8,7 +8,6 @@ relaxedAutoImplicit = false
    weak.linter.mathlibStandardSet = true weak.linter.style.longLine = false maxSynthPendingDepth = 3 - experimental.module = true [[lean_exe]] name = "miscelleaneous"
• mathlib.patch (new)
  • @@ -0,0 +1,52 @@
    + diff --git a/Mathlib/Algebra/Group/ModEq.lean b/Mathlib/Algebra/Group/ModEq.lean + index d35b844522..ba114ce43d 100644 + --- a/Mathlib/Algebra/Group/ModEq.lean + +++ b/Mathlib/Algebra/Group/ModEq.lean + @@ -266,7 +266,7 @@ end ModEq + @[simp] + theorem zsmul_modEq_zsmul [IsAddTorsionFree G] (hn : z ≠ 0) : + z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] := by + - simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm, zsmul_right_inj hn] + + simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm p z _, zsmul_right_inj hn] + + alias ⟨ModEq.zsmul_cancel, _⟩ := zsmul_modEq_zsmul + + diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean + index d88e49e2b0..42e36e1eba 100644 + --- a/Mathlib/Order/CompleteBooleanAlgebra.lean + +++ b/Mathlib/Order/CompleteBooleanAlgebra.lean + @@ -450,7 +450,7 @@ theorem sSup_disjoint_iff {s : Set α} : Disjoint (sSup s) a ↔ ∀ b ∈ s, Di + simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot] + + theorem disjoint_sSup_iff {s : Set α} : Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b := by + - simpa only [disjoint_comm] using @sSup_disjoint_iff + + simpa only [disjoint_comm] using @sSup_disjoint_iff α _ a + + theorem iSup_inf_of_monotone {ι : Type*} [Preorder ι] [IsDirectedOrder ι] {f g : ι → α} + (hf : Monotone f) (hg : Monotone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i := by + diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean + index 46bd529714..a086e8f643 100644 + --- a/Mathlib/Order/Interval/Set/Basic.lean + +++ b/Mathlib/Order/Interval/Set/Basic.lean + @@ -595,7 +595,7 @@ theorem Icc_diff_right : Icc a b \ {b} = Ico a b := + + @[simp] + theorem Ico_diff_left : Ico a b \ {a} = Ioo a b := + - ext fun x => by simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm] + + ext fun x => by grind [← lt_iff_le_and_ne] + + @[simp] + theorem Ioc_diff_right : Ioc a b \ {b} = Ioo a b := + diff --git a/Mathlib/Order/Interval/Set/SuccPred.lean b/Mathlib/Order/Interval/Set/SuccPred.lean + index 9e9a0bdcff..6e76332ddf 100644 + --- a/Mathlib/Order/Interval/Set/SuccPred.lean + +++ b/Mathlib/Order/Interval/Set/SuccPred.lean + @@ -67,7 +67,7 @@ lemma Ico_succ_succ_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : + /-! ##### Inserting into intervals -/ + + lemma insert_Icc_succ_left_eq_Icc (h : a ≤ b) : insert a (Icc (succ a) b) = Icc a b := by + - ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; aesop + + ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; grind [← le_iff_eq_or_succ_le] + + lemma insert_Icc_right_eq_Icc_succ (h : a ≤ succ b) : + insert (succ b) (Icc a b) = Icc a (succ b) := by