fun with supr

Stream: general

[Patrick Massot]

I really need to sleep, so let me offer relaxing exercises again.

lemma supr_split {α ι : Type*} [complete_lattice α] (f : ι → α) (p : ι → Prop) :
(⨆ i, f i) = (⨆ i (h : p i), f i) ⊔ (⨆ i (h : ¬ p i), f i) :=  sorry


lemma supr_split_single {α ι : Type*} [complete_lattice α] (f : ι → α) (i₀ : ι) :
(⨆ i, f i) = f i₀ ⊔ (⨆ i (h : i ≠ i₀), f i) := sorry

[Patrick Massot]

What I actually need is the second one, but I guess the first one is natural too.

[Jalex Stark]

EDIT: got rid of the finish

import tactic

lemma supr_split {α ι : Type*} [complete_lattice α] (f : ι → α) (p : ι → Prop) :
(⨆ i, f i) = (⨆ i (h : p i), f i) ⊔ (⨆ i (h : ¬ p i), f i) :=
begin
  have := @supr_union _ _ _ f {i | p i} {i | ¬ p i},
  dsimp at this, rw ← this, clear this,
  have : ∀ x, (p x ∨ ¬ p x) ↔ true, { tauto!, },
  congr, dsimp,
  ext, rw this, simp,
end

lemma supr_split_single {α ι : Type*} [complete_lattice α] (f : ι → α) (i₀ : ι) :
(⨆ i, f i) = f i₀ ⊔ (⨆ i (h : i ≠ i₀), f i) :=
begin
  rw supr_split, swap, { exact (λ x, x = i₀) },
  congr, simp,
end

[Jalex Stark]

it seems like the current state of this "intern" social technology is "make a new topic in #general or #maths with the sorry, somebody may come along and fill it for you"

[Jalex Stark]

I think it's probably underused

[Jalex Stark]

Patrick, you should delegate whatever sorries you can; I'm happy to trade my time for yours on proof-generation (even if the proof is harder for me, say up to a 3x ratio) because I want to help clear the things that are stopping you from putting out more of a sphere-eversion roadmap. (and probably some others agree, or will find your sorries interesting enough to work on anyway)

[Jesse Michael Han]

you can get supr_split_single with by convert supr_split _ _; simp

[Scott Morrison]

I wonder if we should have a separate "help me with this sorry" stream, specifically for people with PR experience to post in (i.e. not for newbies / learners)

[Scott Morrison]

is there a way to do that without being too elitist? :-)

[Johan Commelin]

I think its fine to just use "general" and "maths" for that

[Johan Commelin]

But if it is decided to start a new stream, may I suggest calling it sorry (not sorry) ? :stuck_out_tongue_wink:

[Patrick Massot]

Thank you very much Jalex. I'm always ashamed when I do that. Note that the two instances were very different. The first one was really a question about automation. I don't think proof assistant have any future if they can't do that kind of work automatically. Unfortunately I messed up the statement because I type \cap when I meant \cup (a decent proof assistant should have raised a warning as the statement was false because of this typo). The second instance if because it was almost 2am and I wanted to finish this proof.

[Patrick Massot]

Yesterday I tried to work late at night because it was too hot all day, but my brain is definitely better at 10am:

lemma supr_split {α ι : Type*} [complete_lattice α] (f : ι → α) (p : ι → Prop) :
(⨆ i, f i) = (⨆ i (h : p i), f i) ⊔ (⨆ i (h : ¬ p i), f i) :=
by simpa [classical.em] using @supr_union _ _ _ f {i | p i} {i | ¬ p i}