Theorem: Nat.recBase2_div2 (Algdata/Data/Nat/Rec.lean)

State before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recBase2 zero one div2 (n + 2) = div2 n (recBase2 zero one div2 (n / 2 + 1))
Tactic:
unfold recBase2
State after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recComplete
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recComplete
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))

State before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recComplete
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recComplete
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Tactic:
rw [recComplete_eq, recComplete_eq]
State after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recCompleteWF
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recCompleteWF
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))

State before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recCompleteWF
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recCompleteWF
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Tactic:
conv =>
  lhs; unfold recCompleteWF
State after:
no goals