Ico_union_right

Stream: Is there code for X?

[Gareth Ma]

Does this code really not exist? Ico is Finset here.

import Mathlib
open Finset
example {a b : ℕ} (h : a ≤ b) : Ico a b.succ = Ico a b ∪ {b} := by
  sorry

[Gareth Ma]

There is List.Ico.succ_top for the list version

[Gareth Ma]

(By the way, how do I use that docs4#List.Ico.succ_top thing?)

[Gareth Ma]

... Like that

[Gareth Ma]

import Mathlib

open Nat Finset

set_option profiler true
set_option trace.profiler true

example {a b : ℕ} (h : a ≤ b) : Ico a b.succ = Ico a b ∪ {b} := by
  ext t
  rw [mem_Ico, mem_union, mem_Ico]
  constructor
  · intro ⟨h1, h2⟩
    by_cases h : t = b
    · rw [h, mem_singleton]
      right
      rfl
    · push_neg at h
      rw [lt_succ] at h2
      have := lt_of_le_of_ne h2 h
      left
      constructor <;> linarith
  · intro h
    cases' h with h h
    · let ⟨h1, h2⟩ := h
      constructor <;> linarith
    · rw [mem_singleton] at h
      constructor <;> linarith

It's true btw, just put together a terrible proof with some tactic abuse

[Gareth Ma]

If someone has a couple minutes, feel free to golf it and pr :(

[Gareth Ma]

I golfed it a little :P

example {a b : ℕ} (ha : a ≤ b) : Ico a b.succ = Ico a b ∪ {b} := by
  ext t
  rw [mem_Ico, mem_union, mem_Ico, lt_succ_iff_lt_or_eq, mem_singleton]
  constructor
  · exact fun ⟨h1, h2⟩ ↦ match h2 with
    | .inl h => .inl ⟨h1, h⟩
    | .inr h => .inr h
  · exact fun h ↦ match h with
    | .inl ⟨h1, h2⟩ => ⟨h1, .inl h2⟩
    | .inr h' => ⟨h'.symm ▸ ha, .inr h'⟩

[Gareth Ma]

(Why does it look completely different :joy: )

[Ruben Van de Velde]

How about this?

import Mathlib
open Finset
example {a b : ℕ} (h : a ≤ b) : Ico a b.succ = Ico a b ∪ {b} := by
  rw [Nat.succ_eq_add_one]
  rw [Nat.Ico_succ_right]
  rw [← Ico_insert_right h]
  rw [@insert_eq]
  rw [@union_comm]

[Gareth Ma]

Ahh thanks a lot. Your first rw is not needed :)

[Ruben Van de Velde]

Yeah, rw_search finds Try this: rw [Nat.Ico_succ_right, @union_comm, ← Ico_insert_right h]

[Yaël Dillies]

docs#Nat.Ico_succ_right_eq_insert_Ico

[Gareth Ma]

lemma Finset.Ico_union_right {a b : ℕ} (h : a ≤ b) : Ico a b ∪ {b} = Ico a b.succ := by
  rw [Ico_succ_right_eq_insert_Ico h, union_comm] ; rfl

yay

[Yaël Dillies]

You should use docs#Finset.insert_eq (or not use ∪ {b} in the first place, really).

[Gareth Ma]

I see, I will change my code for that