Prooving a goal with Or in a special case

Stream: Is there code for X?

[Christian K]

When i normally want to proove a goal that contains Or, I use the left or the right Tactic to proove just one of the Terms. But in this case I have a hypothesis h that says that a variable x is an element of a set S. My goal is that x is in Set B or in Set A. I cannot use the right or the left tactic because not every element in S is in A or in B. The actual proof I need this for has some dependencies, so it wouldn't make sense to include it here.
To illustrate what I mean, here is a minimal example. (This can be proved with simp and apply? but this does not work for my actual proof)

def A := {n : ℕ | n < 10}
def B := {n : ℕ | n ≥ 10}

lemma nat_in_sets (n : Nat) : n ∈ A ∨ n ∈ B := by
  sorry

If you want to see the actual example look here. Scroll down to rotate_A_B_eq_S at line 275. (ignore the rest of the code, it is a mess)

[Niels Voss]

Your goal is definitionally equal to n < 10 ∨ 10 ≤ n so it can be proven with exact Nat.lt_or_ge n 10. However, in more complicated situations, you can use by_cases h : n < 10 which will create two goals, requiring you to prove the theorem separately when h is true and h is false.

[Christian K]

Ok thank you very much, this worked great. With this, I was able to proof that a circle is equidecomposable with a circle with a missing point.