-- Mathlib/Computability/Primrec.lean
theorem list_get? : Primrec₂ (@List.get? α) :=
  let F (l : List α) (n : ℕ) :=
    l.foldl
      (fun (s : ℕ ⊕ α) (a : α) =>
        Sum.casesOn s (@Nat.casesOn (fun _ => ℕ ⊕ α) · (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n)
  have hF : Primrec₂ F :=
    (list_foldl fst (sumInl.comp snd)
      ((sumCasesOn fst (nat_casesOn snd (sumInr.comp <| snd.comp fst) (sumInl.comp snd).to₂).to₂
              (sumInr.comp snd).to₂).comp
          snd).to₂).to₂
  have :
    @Primrec _ (Option α) _ _ fun p : List α × ℕ => Sum.casesOn (F p.1 p.2) (fun _ => none) some :=
    sumCasesOn hF (const none).to₂ (option_some.comp snd).to₂
  this.to₂.of_eq fun l n => by
    dsimp; symm
    induction' l with a l IH generalizing n; · rfl
    rcases n with - | n
    · dsimp [F]
      clear IH
      induction' l with _ l IH <;> simp [*]
    · apply IH

Proof state:
case cons.succ
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
n : ℕ
⊢ (a :: l).get? (n + 1) = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) (n + 1))

Tactic:
apply IH

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)

Tactic:
induction' l with _ l IH <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
l : List α
n : ℕ
⊢ l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)

Tactic:
induction' l with a l IH generalizing n

Result:
case nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
n : ℕ
⊢ [].get? n = Sum.rec (fun val => none) (fun val => some val) (F [] n)

case cons
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
n : ℕ
⊢ (a :: l).get? n = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) n)

Proof state:
case cons
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
n : ℕ
⊢ (a :: l).get? n = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) n)

Tactic:
rcases n with - | n

Result:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
⊢ (a :: l).get? 0 = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) 0)

case cons.succ
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
n : ℕ
⊢ (a :: l).get? (n + 1) = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) (n + 1))

Proof state:
case nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
n : ℕ
⊢ [].get? n = Sum.rec (fun val => none) (fun val => some val) (F [] n)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val => none) (fun val => some val) (F l n) = l.get? n

Tactic:
symm

Result:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
l : List α
n : ℕ
⊢ l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)

Proof state:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
⊢ (a :: l).get? 0 = Sum.rec (fun val => none) (fun val => some val) (F (a :: l) 0)

Tactic:
dsimp [F]

Result:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)

Proof state:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.casesOn (F (l, n).1 (l, n).2) (fun x => none) some = l.get? n

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val => none) (fun val => some val) (F l n) = l.get? n