/-
Copyright (c) 2022 Stuart Presnell. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stuart Presnell

! This file was ported from Lean 3 source module data.nat.even_odd_rec
! leanprover-community/mathlib commit 18a5306c091183ac90884daa9373fa3b178e8607
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Basic
import Mathlib.Init.Data.Nat.Bitwise
/-! # A recursion principle based on even and odd numbers. -/

-- porting note: TODO:
-- Remove dependence on deprecated definitions bit0, bit1.
set_option linter.deprecated false

namespace Nat

/-- Recursion principle on even and odd numbers: if we have `P 0`, and for all `i : ℕ` we can
extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`.
This is nothing more than a wrapper around `Nat.binaryRec`, to avoid having to switch to
dealing with `bit0` and `bit1`. -/

@[elab_as_elim]
def 
evenOddRec: {P : ℕ → Sort ?u.4} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec {
P: ℕ → Sort ?u.4
P : 
ℕ: Type
ℕ → 
Sort _: Type ?u.4
Sort
Sort _: Type ?u.4
 _} (
h0: P 0
h0 : 
P: ℕ → Sort ?u.4
P 
0: ?m.8
0) (
h_even: (n : ℕ) → P n → P (2 * n)
h_even : ∀ (
n: ?m.21
n) (
_: P n
_ : 
P: ℕ → Sort ?u.4
P 
n: ?m.21
n), 
P: ℕ → Sort ?u.4
P (
2: ?m.30
2 * 
n: ?m.21
n))
    (
h_odd: (n : ℕ) → P n → P (2 * n + 1)
h_odd : ∀ (
n: ?m.90
n) (
_: P n
_ : 
P: ℕ → Sort ?u.4
P 
n: ?m.90
n), 
P: ℕ → Sort ?u.4
P (
2: ?m.102
2 * 
n: ?m.90
n + 
1: ?m.112
1)) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
P: ℕ → Sort ?u.4
P 
n: ℕ
n :=
  
binaryRec: {C : ℕ → Sort ?u.232} → C 0 → ((b : Bool) → (n : ℕ) → C n → C (bit b n)) → (n : ℕ) → C n
binaryRec 
h0: P 0
h0 (fun
    | 
false: Bool
false, 
i: ℕ
i, 
hi: P i
hi => (
bit0_val: ∀ (n : ℕ), bit0 n = 2 * n
bit0_val 
i: ℕ
i ▸ 
h_even: (n : ℕ) → P n → P (2 * n)
h_even 
i: ℕ
i 
hi: P i
hi : 
P: ℕ → Sort ?u.4
P (
bit0: {α : Type ?u.267} → [inst : Add α] → α → α
bit0 
i: ℕ
i))
    | 
true: Bool
true, 
i: ℕ
i, 
hi: P i
hi => (
bit1_val: ∀ (n : ℕ), bit1 n = 2 * n + 1
bit1_val 
i: ℕ
i ▸ 
h_odd: (n : ℕ) → P n → P (2 * n + 1)
h_odd 
i: ℕ
i 
hi: P i
hi : 
P: ℕ → Sort ?u.4
P (
bit1: {α : Type ?u.317} → [inst : One α] → [inst : Add α] → α → α
bit1 
i: ℕ
i))) 
n: ℕ
n
#align nat.even_odd_rec 
Nat.evenOddRec: {P : ℕ → Sort u_1} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
Nat.evenOddRec

@[simp]
theorem 
evenOddRec_zero: ∀ (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  evenOddRec h0 h_even h_odd 0 = h0
evenOddRec_zero (
P: ℕ → Sort ?u.740
P : 
ℕ: Type
ℕ → 
Sort _: Type ?u.740
Sort
Sort _: Type ?u.740
 _) (
h0: P 0
h0 : 
P: ℕ → Sort ?u.740
P 
0: ?m.744
0) (
h_even: (i : ℕ) → P i → P (2 * i)
h_even : ∀ 
i: ?m.757
i, 
P: ℕ → Sort ?u.740
P 
i: ?m.757
i → 
P: ℕ → Sort ?u.740
P (
2: ?m.766
2 * 
i: ?m.757
i))
    (
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd : ∀ 
i: ?m.826
i, 
P: ℕ → Sort ?u.740
P 
i: ?m.826
i → 
P: ℕ → Sort ?u.740
P (
2: ?m.838
2 * 
i: ?m.826
i + 
1: ?m.848
1)) : @
evenOddRec: {P : ℕ → Sort ?u.947} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
_: ℕ → Sort ?u.947
_ 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
0: ?m.999
0 = 
h0: P 0
h0 :=
  
binaryRec_zero: ∀ {C : ℕ → Sort ?u.1011} (z : C 0) (f : (b : Bool) → (n : ℕ) → C n → C (bit b n)), binaryRec z f 0 = z
binaryRec_zero 
_: ?m.1012 0
_ 
_: (b : Bool) → (n : ℕ) → ?m.1012 n → ?m.1012 (bit b n)
_
#align nat.even_odd_rec_zero 
Nat.evenOddRec_zero: ∀ (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  evenOddRec h0 h_even h_odd 0 = h0
Nat.evenOddRec_zero

@[simp]
theorem 
evenOddRec_even: ∀ (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → evenOddRec h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n)
evenOddRec_even (
n: ℕ
n : 
ℕ: Type
ℕ) (
P: ℕ → Sort ?u.1089
P : 
ℕ: Type
ℕ → 
Sort _: Type ?u.1089
Sort
Sort _: Type ?u.1089
 _) (
h0: P 0
h0 : 
P: ℕ → Sort ?u.1089
P 
0: ?m.1093
0) (
h_even: (i : ℕ) → P i → P (2 * i)
h_even : ∀ 
i: ?m.1106
i, 
P: ℕ → Sort ?u.1089
P 
i: ?m.1106
i → 
P: ℕ → Sort ?u.1089
P (
2: ?m.1115
2 * 
i: ?m.1106
i))
    (
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd : ∀ 
i: ?m.1175
i, 
P: ℕ → Sort ?u.1089
P 
i: ?m.1175
i → 
P: ℕ → Sort ?u.1089
P (
2: ?m.1187
2 * 
i: ?m.1175
i + 
1: ?m.1197
1)) (
H: h_even 0 h0 = h0
H : 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
0: ?m.1297
0 
h0: P 0
h0 = 
h0: P 0
h0) :
    @
evenOddRec: {P : ℕ → Sort ?u.1304} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
_: ℕ → Sort ?u.1304
_ 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd (
2: ?m.1358
2 * 
n: ℕ
n) = 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
n: ℕ
n (
evenOddRec: {P : ℕ → Sort ?u.1395} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n) :=
  have : ∀ 
a: ?m.1448
a, 
bit: Bool → ℕ → ℕ
bit 
false: Bool
false 
n: ℕ
n = 
a: ?m.1448
a →
      
HEq: {α : Sort ?u.1455} → α → {β : Sort ?u.1455} → β → Prop
HEq (@
evenOddRec: {P : ℕ → Sort ?u.1457} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
_: ℕ → Sort ?u.1457
_ 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
a: ?m.1448
a) (
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
n: ℕ
n (
evenOddRec: {P : ℕ → Sort ?u.1473} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n))
    | _, 
rfl: ∀ {α : Sort ?u.1510} {a : α}, a = a
rfl => by
Goals accomplished! 🐙 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))rw [
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))
evenOddRec: {P : ℕ → Sort ?u.1768} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec,
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (binaryRec h0
    (fun x x_1 x_2 =>
      match x, x_1, x_2 with
      | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
      | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (bit false n))
  (h_even n (evenOddRec h0 h_even h_odd n)) 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))
binaryRec_eq: ∀ {C : ℕ → Sort ?u.1769} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (bit b n)},
  f false 0 z = z → ∀ (b : Bool) (n : ℕ), binaryRec z f (bit b n) = f b n (binaryRec z f n)
binaryRec_eq
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match false, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_even n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0]
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match false, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_even n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0;
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match false, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_even n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))apply 
eq_rec_heq: ∀ {α : Sort ?u.1925} {φ : α → Sort ?u.1924} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
eq_rec_heq
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0;
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))exact 
H: h_even 0 h0 = h0
H
Goals accomplished! 🐙
  
eq_of_heq: ∀ {α : Sort ?u.1679} {a a' : α}, HEq a a' → a = a'
eq_of_heq (
this: ∀ (a : ℕ),
  bit false n = a → HEq (evenOddRec h0 h_even h_odd a) (h_even n (evenOddRec (?m.1500 a) (?m.1501 a) (?m.1502 a) n))
this 
_: ℕ
_ (
bit0_val: ∀ (n : ℕ), bit0 n = 2 * n
bit0_val 
_: ℕ
_))
#align nat.even_odd_rec_even 
Nat.evenOddRec_even: ∀ (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → evenOddRec h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n)
Nat.evenOddRec_even

@[simp]
theorem 
evenOddRec_odd: ∀ (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)
evenOddRec_odd (
n: ℕ
n : 
ℕ: Type
ℕ) (
P: ℕ → Sort ?u.2191
P : 
ℕ: Type
ℕ → 
Sort _: Type ?u.2191
Sort
Sort _: Type ?u.2191
 _) (
h0: P 0
h0 : 
P: ℕ → Sort ?u.2191
P 
0: ?m.2195
0) (
h_even: (i : ℕ) → P i → P (2 * i)
h_even : ∀ 
i: ?m.2208
i, 
P: ℕ → Sort ?u.2191
P 
i: ?m.2208
i → 
P: ℕ → Sort ?u.2191
P (
2: ?m.2217
2 * 
i: ?m.2208
i))
    (
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd : ∀ 
i: ?m.2277
i, 
P: ℕ → Sort ?u.2191
P 
i: ?m.2277
i → 
P: ℕ → Sort ?u.2191
P (
2: ?m.2289
2 * 
i: ?m.2277
i + 
1: ?m.2299
1)) (
H: h_even 0 h0 = h0
H : 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
0: ?m.2399
0 
h0: P 0
h0 = 
h0: P 0
h0) :
    @
evenOddRec: {P : ℕ → Sort ?u.2406} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
_: ℕ → Sort ?u.2406
_ 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd (
2: ?m.2463
2 * 
n: ℕ
n + 
1: ?m.2473
1) = 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n (
evenOddRec: {P : ℕ → Sort ?u.2541} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n) :=
  have : ∀ 
a: ?m.2590
a, 
bit: Bool → ℕ → ℕ
bit 
true: Bool
true 
n: ℕ
n = 
a: ?m.2590
a →
      
HEq: {α : Sort ?u.2597} → α → {β : Sort ?u.2597} → β → Prop
HEq (@
evenOddRec: {P : ℕ → Sort ?u.2599} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
_: ℕ → Sort ?u.2599
_ 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
a: ?m.2590
a) (
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n (
evenOddRec: {P : ℕ → Sort ?u.2615} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec 
h0: P 0
h0 
h_even: (i : ℕ) → P i → P (2 * i)
h_even 
h_odd: (i : ℕ) → P i → P (2 * i + 1)
h_odd 
n: ℕ
n))
    | _, 
rfl: ∀ {α : Sort ?u.2652} {a : α}, a = a
rfl => by
Goals accomplished! 🐙 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))rw [
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))
evenOddRec: {P : ℕ → Sort ?u.2898} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
evenOddRec,
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (binaryRec h0
    (fun x x_1 x_2 =>
      match x, x_1, x_2 with
      | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
      | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (bit true n))
  (h_odd n (evenOddRec h0 h_even h_odd n)) 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))
binaryRec_eq: ∀ {C : ℕ → Sort ?u.2899} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (bit b n)},
  f false 0 z = z → ∀ (b : Bool) (n : ℕ), binaryRec z f (bit b n) = f b n (binaryRec z f n)
binaryRec_eq
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match true, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_odd n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0]
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match true, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_odd n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0;
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq
  (match true, n,
    binaryRec h0
      (fun x x_1 x_2 =>
        match x, x_1, x_2 with
        | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
        | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
      n with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
  (h_odd n (evenOddRec h0 h_even h_odd n))
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))apply 
eq_rec_heq: ∀ {α : Sort ?u.3074} {φ : α → Sort ?u.3073} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
eq_rec_heq
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0;
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

h
(match false, 0, h0 with
  | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
  | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =   h0 
n: ℕ

P: ℕ → Sort u_1

h0: P 0

h_even: (i : ℕ) → P i → P (2 * i)

h_odd: (i : ℕ) → P i → P (2 * i + 1)

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))exact 
H: h_even 0 h0 = h0
H
Goals accomplished! 🐙
  
eq_of_heq: ∀ {α : Sort ?u.2821} {a a' : α}, HEq a a' → a = a'
eq_of_heq (
this: ∀ (a : ℕ),
  bit true n = a → HEq (evenOddRec h0 h_even h_odd a) (h_odd n (evenOddRec (?m.2642 a) (?m.2643 a) (?m.2644 a) n))
this 
_: ℕ
_ (
bit1_val: ∀ (n : ℕ), bit1 n = 2 * n + 1
bit1_val 
_: ℕ
_))
#align nat.even_odd_rec_odd 
Nat.evenOddRec_odd: ∀ (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)
Nat.evenOddRec_odd

end Nat