Feat: Add computable rec for Option via rec_eq_recC pattern (#3255)

Adds a computable recursor for `Option`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Option/Basic.lean

@@ -362,6 +362,26 @@ theorem casesOn'_none_coe (f : Option α → β) (o : Option α) :
     casesOn' o (f none) (f ∘ (fun a ↦ ↑a)) = f o := by cases o <;> rfl
 #align option.cases_on'_none_coe Option.casesOn'_none_coe
 
+-- porting note: workaround for leanprover/lean4#2049
+section recursor_workarounds
+
+/-- A computable version of `Option.rec`. Workaround until Lean has native support for this. -/
+def recC.{u_1, u} {α : Type u} {motive : Option α → Sort u_1} (none : motive none)
+  (some : (val : α) →  motive (some val)) :
+    (t : Option α) → motive t
+| Option.none => none
+| Option.some a => some a
+
+@[csimp]
+lemma rec_eq_recC : @Option.rec = @Option.recC := by
+  ext α motive none some o
+  induction o with
+  | none => rfl
+  | some a =>
+    rw [Option.recC]
+
+end recursor_workarounds
+
 theorem orElse_eq_some (o o' : Option α) (x : α) :
     (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x := by
   cases o