Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
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 nP (2 * n)) → ((n : ) → P nP (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 nP (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 nP (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 nC (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 nP (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 nP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
Nat.evenOddRec
@[simp] theorem
evenOddRec_zero: ∀ (P : Sort u_1) (h0 : P 0) (h_even : (i : ) → P iP (2 * i)) (h_odd : (i : ) → P iP (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 iP (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 iP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
_: Sort ?u.947
_
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (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 nC (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 iP (2 * i)) (h_odd : (i : ) → P iP (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 iP (2 * i)) (h_odd : (i : ) → P iP (2 * i + 1)), h_even 0 h0 = h0evenOddRec 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 iP (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 iP (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 iP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
_: Sort ?u.1304
_
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
(
2: ?m.1358
2
*
n:
n
) =
h_even: (i : ) → P iP (2 * i)
h_even
n:
n
(
evenOddRec: {P : Sort ?u.1395} → P 0((n : ) → P nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
_: Sort ?u.1457
_
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
a: ?m.1448
a
) (
h_even: (i : ) → P iP (2 * i)
h_even
n:
n
(
evenOddRec: {P : Sort ?u.1473} → P 0((n : ) → P nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
n:
n
)) | _,
rfl: ∀ {α : Sort ?u.1510} {a : α}, a = a
rfl
=>

Goals accomplished! 🐙
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_even n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_even n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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) ()) (h_even n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_even n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_even n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_even n (evenOddRec h0 h_even h_odd n))

Goals accomplished! 🐙
eq_of_heq: ∀ {α : Sort ?u.1679} {a a' : α}, HEq a a'a = a'
eq_of_heq
(
this: ∀ (a : ), = aHEq (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 iP (2 * i)) (h_odd : (i : ) → P iP (2 * i + 1)), h_even 0 h0 = h0evenOddRec 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 iP (2 * i)) (h_odd : (i : ) → P iP (2 * i + 1)), h_even 0 h0 = h0evenOddRec 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 iP (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 iP (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 iP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
_: Sort ?u.2406
_
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
(
2: ?m.2463
2
*
n:
n
+
1: ?m.2473
1
) =
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
n:
n
(
evenOddRec: {P : Sort ?u.2541} → P 0((n : ) → P nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (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 nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
_: Sort ?u.2599
_
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
a: ?m.2590
a
) (
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
n:
n
(
evenOddRec: {P : Sort ?u.2615} → P 0((n : ) → P nP (2 * n)) → ((n : ) → P nP (2 * n + 1)) → (n : ) → P n
evenOddRec
h0: P 0
h0
h_even: (i : ) → P iP (2 * i)
h_even
h_odd: (i : ) → P iP (2 * i + 1)
h_odd
n:
n
)) | _,
rfl: ∀ {α : Sort ?u.2652} {a : α}, a = a
rfl
=>

Goals accomplished! 🐙
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_odd n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_odd n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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) ()) (h_odd n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_odd n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_odd n (evenOddRec h0 h_even h_odd n))
n:

P: Sort u_1

h0: P 0

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

h_odd: (i : ) → P iP (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 iP (2 * i)

h_odd: (i : ) → P iP (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 iP (2 * i)

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

H: h_even 0 h0 = h0

HEq (evenOddRec h0 h_even h_odd ()) (h_odd n (evenOddRec h0 h_even h_odd n))

Goals accomplished! 🐙
eq_of_heq: ∀ {α : Sort ?u.2821} {a a' : α}, HEq a a'a = a'
eq_of_heq
(
this: ∀ (a : ), = aHEq (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 iP (2 * i)) (h_odd : (i : ) → P iP (2 * i + 1)), h_even 0 h0 = h0evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)
Nat.evenOddRec_odd
end Nat