long cases but only two proofs

Stream: general

[Ira Fesefeldt]

I have a very big inductive definition. But I often need to prove something only for the one case and for all other cases (together). I currently work with meta variables. But this seem to be very slow, since Lean now checks the proof for every of those cases. Is there a way to make this more idiomatic/more performed?

An illustrative example may be this:

inductive BigDef where
  | a : BigDef
  | b : BigDef
  | c : BigDef
  | d : BigDef

open BigDef

def f : BigDef → Nat
  | a => 0
  | b => 1
  | c => 2
  | d => 3

example : f x = 1 ↔ x = b := by
  cases x with
  | b =>
    simp [f] -- proof 1
  | _ =>
    simp [f] -- proof 2

In this case, the proof 1 and 2 are here actually the same. This is mere because the example may already be too simple... In general I have two different proofs. Proof 2 however takes rather long, since Lean checks this for every case of x.

[Edward van de Meent]

what is the #xy here?
it might be the case that there is a better way than using an inductive type to encode this problem...

[Ira Fesefeldt]

In my use case, the inductive type I am working with is a program and the function f is a probability transition function

[Edward van de Meent]

could it be useful to write the program as multiple definitions which are mutually inductive?

[Ira Fesefeldt]

You mean in order to group statements with similar proofs?