Inductively proving that a number is either even or odd in Lean

Question

I have the following Lean definitions:

def is_even (a : Nat) := ∃ m, a = 2 * m
def is_odd (a: Nat) := ∃ m, a = 2 * m + 1

The following proof would be complete if I knew how to actually perform the induction

theorem is_even_or_odd: is_even a ∨ is_odd a :=
  have even_plus_one_is_odd : ∀ x, is_even x → is_odd (x + 1) := fun x => fun h => 
  even_plus_odd_is_odd h one_is_odd

  have odd_plus_one_is_even: ∀ x, is_odd x → is_even (x + 1) := fun x => fun h => 
  odd_plus_odd_is_even h one_is_odd

  have zero_is_even: is_even 0 := zero_is_even

  have inductive_step: ∀ x, is_even x ∨ is_odd x → is_even (x + 1) ∨ is_odd (x + 1) :=
    fun x => fun h => h.elim
      (fun h1 => Or.inr (even_plus_one_is_odd x h1))
      (fun h2 => Or.inl (odd_plus_one_is_even x h2))

  -- Using induction, (is_even a ∨ is_odd a) holds for every number
  sorry

I read about induction on lean-lang.org and had trouble understanding it. A completion of this proof with either term or tactic mode induction would be appreciated!

Answer 1

Here's a completed proof, which should be inserted at the place of your sorry:

  by
  induction a;
  . apply Or.inl; exact zero_is_even;
  . apply inductive_step; assumption;

You start a proof by by to enter the tactic mode, then use the induction tactic as introduced here, then proceed normally.