疑問:並列になっている cases を match のように同時分解したい

[Seasawher]

仮定 P1 : A1 ∨ B1 と P2 : A2 ∨ B2 があって，P1 と P2 の間に関係がなく，P1 と P2 について分岐する証明を書きたいとき， cases を利用するとどうしても P1 か P2 のどちらかを先に分解しないといけない．つまり，分岐のネストが深くなってしまう．

しかし，P1 と P2 は独立なので同時に分解したい．ちょうど match によるパターンマッチのように．

↓ 例

def de_morgan := ∀ (p q : Prop), ¬(p ∧ q) → (¬p) ∨ (¬q)

def weak_em := ∀ (p : Prop), ¬ p ∨ ¬ ¬ p

theorem currying (p q : Prop) : ¬ (p ∧ q) ↔ (p → ¬ q) := by 
  constructor

  case mp =>
    intro h hp hq
    have : p ∧ q := ⟨hp, hq⟩
    contradiction

  case mpr =>
    intro h hand
    obtain ⟨hp, hq⟩ := hand
    have := h hp
    contradiction

theorem de_morgan_iff_weak_em : de_morgan ↔ weak_em := by
  constructor

  case mp =>
    intro h p
    have := h p
    apply this
    intro nand
    obtain ⟨hp, hnp⟩ := nand
    apply hnp
    assumption

  case mpr =>
    intro h p q hpq
    have em_p := h p
    have em_q := h q
    cases em_p
    case inl =>
      left; assumption
    case inr nnp =>
      cases em_q
      case inl => right; assumption
      case inr nnq =>
        exfalso
        apply nnp
        intro hp
        rw [currying] at hpq
        have := hpq hp
        contradiction

#print axioms de_morgan_iff_weak_em

[Seasawher]

see: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.60cases.60.20for.20multiple.20independent.20.60or.60.20statements/near/444883689

[Seasawher]

無理そう