If it's not sum.inr then it's sum.inr

Stream: Is there code for X?

[Eric Wieser]

Is there a better way to state ∀ i, ¬∃ (i' : α), sum.inl i' = i → ∃ (i' : α), sum.inr i' = i?

[Eric Wieser]

(it's obviously an iff, but I only need that direction)

[Reid Barton]

probably using or (and more parentheses)

[Reid Barton]

and a lemma on or

[Eric Wieser]

To un-xy, I want to split a sum over x into the cases when f x is sum.inl x' and sum.inr x'

[Adam Topaz]

cases f x doesn't work?

[Eric Wieser]

And right now I do it by inserting if ( ∃ (i' : α), sum.inl i' = f i) then g x else g x then using docs#finset.sum_ite

[Eric Wieser]

If I used sum.elim, then I'd need a different finset lemma

[Eric Wieser]

Oh, I'm looking for that "make conjunction/disjunction of inductive" command, I think?

[Reid Barton]

hmm is that the only lemma with a sum of two sums on the right?

[Adam Topaz]

(∃ b : β, f x = sum.inl b) ∨ (∃ c : γ, f x = sum.inr c) ?

[Reid Barton]

How about docs#finset.sum_sum_elim

[Reid Barton]

this also might not be ideally stated

[Eric Wieser]

Oh that would be perfect. Whoops. I assumed it would be more general so I could use it on arbitrary enum-like typee

[Reid Barton]

It would be nice if it just had h x on the left, and h (sum.inl x) and h (sum.inr x) on the right

[Eric Wieser]

Yeah, you're right that the current statement isn't enough for me

[Eric Wieser]

Is there a version of mk_iff_of_inductive_prop that works for data and produces existentials?

[Eric Wieser]

Coming back to this with lean accessible - the best statement I can come up with is:

example {α β γ δ : Type*} [fintype γ] [comm_monoid δ] (f : γ → α ⊕ β) (g : γ → δ) :
  ∏ (i : γ), g i = ∏ (i : γ) in finset.univ.filter (λ i, ∃ i', f i = sum.inl i'), g i *
                   ∏ (i : γ) in finset.univ.filter (λ i, ∃ i', f i = sum.inr i'), g i := sorry

or for a more general case

example {α β γ δ : Type*} [fintype γ] [comm_monoid δ] (f : γ → α ⊕ β) (g : γ → α → δ) (h : γ → β → δ) :
  ∏ (i : γ), (f i).elim (g i) (h i) =
                   ∏ (i : {i : γ // ∃ i', f i = sum.inl i'}), g i (classical.some i.prop) *
                   ∏ (i : {i : γ // ∃ i', f i = sum.inr i'}), h i (classical.some i.prop) := sorry

Can you think of a better theorem statement?

[Reid Barton]

the first one is just a special case of product over a disjoint union right?

[Reid Barton]

These right-hand sides look pretty unpleasant

[Eric Wieser]

Yes, it is - do we have a lemma for that already?

[Reid Barton]

surely, but I don't think it really helps you

[Reid Barton]

Because it's not making progress overall

[Reid Barton]

I think you want the variation of sum_sum_elim I suggested earlier

[Eric Wieser]

The difficulty is I'm not splitting over the summand, I'm splitting over some function of it

[Reid Barton]

Oh I missed that

[Reid Barton]

I don't know, this is too abstract I think

[Reid Barton]

I mean a lemma only helps if the new expression is actually easier to deal with

[Reid Barton]

There must be some reason why knowing what side f i is in helps you evaluate the sum

[Reid Barton]

and that reason will determine what kind of lemma you need

[Reid Barton]

but in general, there's docs#finset.sum_union :shrug:

[Eric Wieser]

Perhaps I should just push forward with what I have, and ask again once I have a working proof

[Eric Wieser]

You were right, I didn't need this

[Mario Carneiro]

This looks like cases e : f x

[Eric Wieser]

Indeed - although I thought I need to split the sum before I had x available

[Mario Carneiro]

so like list.partition then?

[Eric Wieser]

Well, except on a finset

[Mario Carneiro]

there is a theorem about partitioning a finset using finset.filter

[Mario Carneiro]

I think the problem needs some more un-#xy

[Eric Wieser]

I got what I needed with something completely different (in #5269, alternating.lean:590, with by_cases). The PR hasn't been cleaned up yet, but once it has been I'd appreciate suggestions for shortening the proof