Instances on sum components

Stream: mathlib4

[Sébastien Gouëzel]

I want to define an auxiliary type as a sum. I can not have Lean realize that, since all components of the sum satisfy some instance, then all components of the sum satisfy this instance (yes, I wrote the same thing twice). Example:

import Mathlib.RingTheory.Bezout

variable (R : Type) [Ring R]

@[reducible] def two_rings : Unit ⊕ Unit → Type
  | Sum.inl _ => R
  | Sum.inr _ => R

lemma foo (i : Unit ⊕ Unit) : Ring (two_rings R i) := by infer_instance -- fails

lemma bar : (i : Unit ⊕ Unit) → Ring (two_rings R i)  -- works
  | Sum.inl _ | Sum.inr _ => by infer_instance

In my case, it's a topological module structure. I can define all the instances by hand just like for bar above, but I wonder if I'm missing some construction to make this automatic for typeclass inference.

[Eric Wieser]

I asked about this a long time ago here

[Sébastien Gouëzel]

It's funny, I need this also for multilinear maps (but in my use case the two types along inl and inr are not the same, so I can't really take a shortcut...)

[Matthew Ballard]

It seems like you want something like the deriving handler for instances on types with finitely many terms to apply Pi.ring etc

[Sébastien Gouëzel]

It's not a Pi instance, as I'm not asking to show that the global object has some typeclass. I'm only asking that each component should have some instance detected by typeclass inference, given the fact that each component has the instance to start with. It's completely tautological (or syntaxical?).

[Matthew Ballard]

Oh ok. You want the hypothesis of Pi.ring

[Yaël Dillies]

Still, it sounds like it could be a job for deriving

[Eric Wieser]

If we involve a metaprogram here, note that we probably also want to have instances for Option.rec, Sigma.rec, Nat.rec, Weekday.rec, ...

[Eric Wieser]

#11780 adds a bunch of instances along these lines; is it a coincidence that @Amelia Livingston wanted this too, or did this thread spin out of LFTCM 2024?

[Kevin Buzzard]

I think it's a coincidence? Amelia asked me this question the day after Sebastian made his post and I pointed her to it.

[Amelia Livingston]

Yeah, just a coincidence. I don't really need #11780 or #11810 for anything - I'm not sure if the other members of my LFTCM group are planning on PR'ing their work - just thought I might as well PR, but I can close them if we should be using a metaprogram instead (edit: although I've just seen you've reviewed #11780, Eric, thank you!)