[STATEMENT]
lemma disj_four_cases:
  assumes "A \<or> B \<or> C \<or> D" and "A \<Longrightarrow> P" and "B \<Longrightarrow> P" and "C \<Longrightarrow> P" and "D \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<or> B \<or> C \<or> D
A \<Longrightarrow> P
B \<Longrightarrow> P
C \<Longrightarrow> P
D \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto