Map from sum in standard lib?

Stream: general

[Benedikt Ahrens]

Is a function similar to this one (and a notation for it) available in the standard library?

def map_from_sum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C
| (sum.inl a) := f a
| (sum.inr b) := g b

Thanks, Benedikt

[Kevin Buzzard]

You're really here to check that your students aren't cheating in your Lean course, right? ;-)

[Kevin Buzzard]

I was expecting to lay my hands on that function at once, but I can't immediately find it.

[Kevin Buzzard]

or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c but I couldn't spot sum.elim

[Kevin Buzzard]

oh found it, it's in data.sum

[Kevin Buzzard]

ha ha, I didn't even know that file existed.

import data.sum

#check @sum.elim
/-
sum.elim : Π {α : Type u_1} {β : Type u_2} {γ : Sort u_3}, (α → γ) → (β → γ) → α ⊕ β → γ
-/

[Reid Barton]

Nice, I didn't know this existed either. Non-dependent eliminators are frequently more convenient, I wish Lean would generate them automatically.

[Bryan Gin-ge Chen]

I was surprised that suggest didn't help:

import tactic
import data.sum

def map_from_sum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C := by suggest
/- There are no applicable declarations
state:
A B C : Type,
f : A → C,
g : B → C
⊢ A ⊕ B → C -/

[Kevin Buzzard]

Might be because it's data not a prop?

[Bryan Gin-ge Chen]

Ah, that makes sense. This reminds me of how we couldn't use cc on your "random types" challenge.

[Benedikt Ahrens]

Thanks a lot for your answers.
I tried hard to find empty.elim (or another map of type empty -> C), but have not been successful. Is such a map pre-defined?

[Rob Lewis]

empty.elim does exist (in mathlib, logic.basic, one of the very first imports). There's also empty.rec and empty.rec_on in core.

[Bryan Gin-ge Chen]

It's just logic.basic, not data.logic.basic.

[Rob Lewis]

I was also surprised suggest didn't find this. Maybe suggest shouldn't filter out Sort * declarations? @Scott Morrison