sum.elim on function operations

Stream: Is there code for X?

[Yaël Dillies]

Do we have the following lemmas?

import algebra.module.pi

example (α β γ : Type*) [has_add γ] (f₀ f₁ : α → γ) (g₀ g₁ : β → γ) :
  sum.elim f₀ g₀ + sum.elim f₁ g₁ = sum.elim (f₀ + f₁) (g₀ + g₁) :=
by ext (a | b); simp

example (α β γ δ : Type*) [has_vadd γ δ]
  (f₀ : α → γ) (g₀ : β → γ) (f₁ : α → δ) (g₁ : β → δ) :
  sum.elim f₀ g₀ +ᵥ sum.elim f₁ g₁ = sum.elim (f₀ +ᵥ f₁) (g₀ +ᵥ g₁) :=
by ext (a | b); simp

example (α β γ : Type*) [has_mul γ] (f₀ f₁ : α → γ) (g₀ g₁ : β → γ) :
  sum.elim f₀ g₀ * sum.elim f₁ g₁ = sum.elim (f₀ * f₁) (g₀ * g₁) :=
by ext (a | b); simp

example (α β γ δ : Type*) [has_scalar γ δ]
  (f₀ : α → γ) (g₀ : β → γ) (f₁ : α → δ) (g₁ : β → δ) :
  sum.elim f₀ g₀ • sum.elim f₁ g₁ = sum.elim (f₀ • f₁) (g₀ • g₁) :=
by ext (a | b); simp

[Eric Wieser]

Note this is a can of worms; such statements are true for almost every recursor

[Yaël Dillies]

Erhm, yeah I guess

[Eric Wieser]

I think I asked a related question a while ago about has_add (sum.elim f g s) where f : α → Type*, g : β → Type*.