Confusion about cases'

Stream: new members

[Chengyan Hu]

It seems like in lean we can only deconstruct hypothesis in form of P \or Q, P \and Q. If I want to deal with h:P \or Q -> R the only thing I can do is apply it to hR:R or the goal R. I'm not that sure if my understanding is correct or not, and this fact seems tedious for me, is there any easier way to deal with that?

[Aaron Liu]

How do you expect this to be destructed?

[Aaron Liu]

That is, given a h : P ∨ Q → R, what do you want to turn this into to make it easier to use?

[Chengyan Hu]

I mean, I would like to use P->R and Q->R

[Aaron Liu]

You can rw with docs#or_imp

[Kyle Miller]

And here's a way you can find or_imp:

example (p q r : Prop) : (p ∨ q → r) ↔ ((p → r) ∧ (q → r)) := by exact?
-- Try this: exact or_imp

[Chengyan Hu]

I see! Thx a lot