How to prove by case analysis on a logical condition being either true or false in Isabelle/HOL?

I know that Isabelle can do case analysis by constructors (e.g. of a list), but

Is there a way to split into cases based on whether a condition is true or false?

For example, in proving the following lemma, my logic (as indicated by the following invalid proof in invalid syntax), is that if the condition "x ∈ A" is true, the proof simplifies to something trivial; it also simplifies when the condition is false (i.e. "x ∉ A"):

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (case "x ∈ A")
  (* ... case true *)
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  have "x ∈ B ∧ x ∈ C" by simp
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)

But I don't know how to translate this "case analysis" in English into Isabelle.

Is there way in Isabelle/HOL to express this kind of case analysis by the true or false of a condition? (as of Isabelle 2021)

(Or does it require additional axioms such as the law of excluded middle?)

Solution

You've almost correctly guessed the syntax, you can write a proof by cases for any predicate with the syntax proof (cases "<pred>").

For the example you provided:

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (cases "x ∈ A")
  (* ... case true *)
  case True
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  case False
  then have "x ∈ B ∧ x ∈ C" sorry (* by simp*)
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)