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: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro

! This file was ported from Lean 3 source module data.nat.size
! 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.Pow
import Mathlib.Data.Nat.Bits

namespace Nat

/-! ### `shiftl` and `shiftr` -/

section
set_option linter.deprecated false

theorem shiftl_eq_mul_pow: โ (m n : โ), shiftl m n = m * 2 ^ nshiftl_eq_mul_pow (m: โm) : โ n: ?m.6n, shiftl: โ โ โ โ โshiftl m: ?m.2m n: ?m.6n = m: ?m.2m * 2: ?m.172 ^ n: ?m.6n
| 0: โ0 => (Nat.mul_one: โ (n : โ), n * 1 = nNat.mul_one _: โ_).symm: โ {ฮฑ : Sort ?u.139} {a b : ฮฑ}, a = b โ b = asymm
| k: โk + 1 => byGoals accomplished! ๐
m, k: โshiftl m (k + 1) = m * 2 ^ (k + 1)show bit0: {ฮฑ : Type ?u.308} โ [inst : Add ฮฑ] โ ฮฑ โ ฮฑbit0 (shiftl: โ โ โ โ โshiftl m: โm k: โk) = m: โm * (2: ?m.3262 ^ k: โk * 2: ?m.3362)m, k: โbit0 (shiftl m k) = m * (2 ^ k * 2)
m, k: โshiftl m (k + 1) = m * 2 ^ (k + 1)rw [m, k: โbit0 (shiftl m k) = m * (2 ^ k * 2)bit0_val: โ (n : โ), bit0 n = 2 * nbit0_val,m, k: โ2 * shiftl m k = m * (2 ^ k * 2) m, k: โbit0 (shiftl m k) = m * (2 ^ k * 2)shiftl_eq_mul_pow: โ (m n : โ), shiftl m n = m * 2 ^ nshiftl_eq_mul_pow m: โm k: โk,m, k: โ2 * (m * 2 ^ k) = m * (2 ^ k * 2) m, k: โbit0 (shiftl m k) = m * (2 ^ k * 2)mul_comm: โ {G : Type ?u.728} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm 2: ?m.7322,m, k: โm * 2 ^ k * 2 = m * (2 ^ k * 2) m, k: โbit0 (shiftl m k) = m * (2 ^ k * 2)mul_assoc: โ {G : Type ?u.791} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocm, k: โm * (2 ^ k * 2) = m * (2 ^ k * 2)]Goals accomplished! ๐
#align nat.shiftl_eq_mul_pow Nat.shiftl_eq_mul_pow: โ (m n : โ), shiftl m n = m * 2 ^ nNat.shiftl_eq_mul_pow

theorem shiftl'_tt_eq_mul_pow: โ (m n : โ), shiftl' true m n + 1 = (m + 1) * 2 ^ nshiftl'_tt_eq_mul_pow (m: โm) : โ n: ?m.895n, shiftl': Bool โ โ โ โ โ โshiftl' true: Booltrue m: ?m.891m n: ?m.895n + 1: ?m.9031 = (m: ?m.891m + 1: ?m.9251) * 2: ?m.9392 ^ n: ?m.895n
| 0: โ0 => byGoals accomplished! ๐ m: โshiftl' true m 0 + 1 = (m + 1) * 2 ^ 0simp [shiftl: โ โ โ โ โshiftl, shiftl': Bool โ โ โ โ โ โshiftl', pow_zero: โ (n : โ), n ^ 0 = 1pow_zero, Nat.one_mul: โ (n : โ), 1 * n = nNat.one_mul]Goals accomplished! ๐
| k: โk + 1 => byGoals accomplished! ๐
m, k: โshiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)change bit1: {ฮฑ : Type ?u.1700} โ [inst : One ฮฑ] โ [inst : Add ฮฑ] โ ฮฑ โ ฮฑbit1 (shiftl': Bool โ โ โ โ โ โshiftl' true: Booltrue m: โm k: โk) + 1: ?m.17291 = (m: โm + 1: ?m.17511) * (2: ?m.17682 ^ k: โk * 2: ?m.17782)m, k: โbit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
m, k: โshiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)rw [m, k: โbit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)bit1_val: โ (n : โ), bit1 n = 2 * n + 1bit1_valm, k: โ2 * shiftl' true m k + 1 + 1 = (m + 1) * (2 ^ k * 2)]m, k: โ2 * shiftl' true m k + 1 + 1 = (m + 1) * (2 ^ k * 2)
m, k: โshiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)change 2: ?m.22152 * (shiftl': Bool โ โ โ โ โ โshiftl' true: Booltrue m: โm k: โk + 1: ?m.22281) = _: ?m.2248_m, k: โ2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)
m, k: โshiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)rw [m, k: โ2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)shiftl'_tt_eq_mul_pow: โ (m n : โ), shiftl' true m n + 1 = (m + 1) * 2 ^ nshiftl'_tt_eq_mul_pow m: โm k: โk,m, k: โ2 * ((m + 1) * 2 ^ k) = (m + 1) * (2 ^ k * 2) m, k: โ2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)mul_left_comm: โ {G : Type ?u.2354} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)mul_left_comm,m, k: โ(m + 1) * (2 * 2 ^ k) = (m + 1) * (2 ^ k * 2) m, k: โ2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)mul_comm: โ {G : Type ?u.2391} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm 2: ?m.23952m, k: โ(m + 1) * (2 ^ k * 2) = (m + 1) * (2 ^ k * 2)]Goals accomplished! ๐
#align nat.shiftl'_tt_eq_mul_pow Nat.shiftl'_tt_eq_mul_pow: โ (m n : โ), shiftl' true m n + 1 = (m + 1) * 2 ^ nNat.shiftl'_tt_eq_mul_pow

end

theorem one_shiftl: โ (n : โ), shiftl 1 n = 2 ^ none_shiftl (n: ?m.2511n) : shiftl: โ โ โ โ โshiftl 1: ?m.25161 n: ?m.2511n = 2: ?m.25302 ^ n: ?m.2511n :=
(shiftl_eq_mul_pow: โ (m n : โ), shiftl m n = m * 2 ^ nshiftl_eq_mul_pow _: โ_ _: โ_).trans: โ {ฮฑ : Sort ?u.2590} {a b c : ฮฑ}, a = b โ b = c โ a = ctrans (Nat.one_mul: โ (n : โ), 1 * n = nNat.one_mul _: โ_)
#align nat.one_shiftl Nat.one_shiftl: โ (n : โ), shiftl 1 n = 2 ^ nNat.one_shiftl

@[simp]
theorem zero_shiftl: โ (n : โ), shiftl 0 n = 0zero_shiftl (n: โn) : shiftl: โ โ โ โ โshiftl 0: ?m.26200 n: ?m.2615n = 0: ?m.26310 :=
(shiftl_eq_mul_pow: โ (m n : โ), shiftl m n = m * 2 ^ nshiftl_eq_mul_pow _: โ_ _: โ_).trans: โ {ฮฑ : Sort ?u.2651} {a b c : ฮฑ}, a = b โ b = c โ a = ctrans (Nat.zero_mul: โ (n : โ), 0 * n = 0Nat.zero_mul _: โ_)
#align nat.zero_shiftl Nat.zero_shiftl: โ (n : โ), shiftl 0 n = 0Nat.zero_shiftl

theorem shiftr_eq_div_pow: โ (m n : โ), shiftr m n = m / 2 ^ nshiftr_eq_div_pow (m: โm) : โ n: ?m.2687n, shiftr: โ โ โ โ โshiftr m: ?m.2683m n: ?m.2687n = m: ?m.2683m / 2: ?m.26982 ^ n: ?m.2687n
| 0: โ0 => (Nat.div_one: โ (n : โ), n / 1 = nNat.div_one _: โ_).symm: โ {ฮฑ : Sort ?u.2814} {a b : ฮฑ}, a = b โ b = asymm
| k: โk + 1 =>
(congr_arg: โ {ฮฑ : Sort ?u.2923} {ฮฒ : Sort ?u.2922} {aโ aโ : ฮฑ} (f : ฮฑ โ ฮฒ), aโ = aโ โ f aโ = f aโcongr_arg div2: โ โ โdiv2 (shiftr_eq_div_pow: โ (m n : โ), shiftr m n = m / 2 ^ nshiftr_eq_div_pow m: โm k: โk)).trans: โ {ฮฑ : Sort ?u.2931} {a b c : ฮฑ}, a = b โ b = c โ a = ctrans <| byGoals accomplished! ๐
m, k: โdiv2 (m / 2 ^ k) = m / 2 ^ (k + 1)rw [m, k: โdiv2 (m / 2 ^ k) = m / 2 ^ (k + 1)div2_val: โ (n : โ), div2 n = n / 2div2_val,m, k: โm / 2 ^ k / 2 = m / 2 ^ (k + 1) m, k: โdiv2 (m / 2 ^ k) = m / 2 ^ (k + 1)Nat.div_div_eq_div_mul: โ (m n k : โ), m / n / k = m / (n * k)Nat.div_div_eq_div_mul,m, k: โm / (2 ^ k * 2) = m / 2 ^ (k + 1) m, k: โdiv2 (m / 2 ^ k) = m / 2 ^ (k + 1)Nat.pow_succ: โ (n m : โ), n ^ succ m = n ^ m * nNat.pow_succm, k: โm / (2 ^ k * 2) = m / (2 ^ k * 2)]Goals accomplished! ๐
#align nat.shiftr_eq_div_pow Nat.shiftr_eq_div_pow: โ (m n : โ), shiftr m n = m / 2 ^ nNat.shiftr_eq_div_pow

@[simp]
theorem zero_shiftr: โ (n : โ), shiftr 0 n = 0zero_shiftr (n: โn) : shiftr: โ โ โ โ โshiftr 0: ?m.31580 n: ?m.3153n = 0: ?m.31690 :=
(shiftr_eq_div_pow: โ (m n : โ), shiftr m n = m / 2 ^ nshiftr_eq_div_pow _: โ_ _: โ_).trans: โ {ฮฑ : Sort ?u.3189} {a b c : ฮฑ}, a = b โ b = c โ a = ctrans (Nat.zero_div: โ (b : โ), 0 / b = 0Nat.zero_div _: โ_)
#align nat.zero_shiftr Nat.zero_shiftr: โ (n : โ), shiftr 0 n = 0Nat.zero_shiftr

theorem shiftl'_ne_zero_left: โ (b : Bool) {m : โ}, m โ  0 โ โ (n : โ), shiftl' b m n โ  0shiftl'_ne_zero_left (b: ?m.3221b) {m: ?m.3224m} (h: m โ  0h : m: ?m.3224m โ  0: ?m.32300) (n: ?m.3243n) : shiftl': Bool โ โ โ โ โ โshiftl' b: ?m.3221b m: ?m.3224m n: ?m.3243n โ  0: ?m.32490 := byGoals accomplished! ๐
b: Boolm: โh: m โ  0n: โshiftl' b m n โ  0induction n: โnb: Boolm: โh: m โ  0zeroshiftl' b m zero โ  0b: Boolm: โh: m โ  0nโ: โn_ihโ: shiftl' b m nโ โ  0succshiftl' b m (succ nโ) โ  0 b: Boolm: โh: m โ  0n: โshiftl' b m n โ  0<;>b: Boolm: โh: m โ  0zeroshiftl' b m zero โ  0b: Boolm: โh: m โ  0nโ: โn_ihโ: shiftl' b m nโ โ  0succshiftl' b m (succ nโ) โ  0 b: Boolm: โh: m โ  0n: โshiftl' b m n โ  0simp [bit_ne_zero: โ (b : Bool) {n : โ}, n โ  0 โ bit b n โ  0bit_ne_zero, shiftl': Bool โ โ โ โ โ โshiftl', *]Goals accomplished! ๐
#align nat.shiftl'_ne_zero_left Nat.shiftl'_ne_zero_left: โ (b : Bool) {m : โ}, m โ  0 โ โ (n : โ), shiftl' b m n โ  0Nat.shiftl'_ne_zero_left

theorem shiftl'_tt_ne_zero: โ (m : โ) {n : โ}, n โ  0 โ shiftl' true m n โ  0shiftl'_tt_ne_zero (m: โm) : โ {n: ?m.3509n}, (n: ?m.3509n โ  0: ?m.35160) โ shiftl': Bool โ โ โ โ โ โshiftl' true: Booltrue m: ?m.3505m n: ?m.3509n โ  0: ?m.35310
| 0: โ0, h: 0 โ  0h => absurd: โ {a : Prop} {b : Sort ?u.3574}, a โ ยฌa โ babsurd rfl: โ {ฮฑ : Sort ?u.3577} {a : ฮฑ}, a = arfl h: 0 โ  0h
| succ: โ โ โsucc _, _ => Nat.bit1_ne_zero: โ (n : โ), bit1 n โ  0Nat.bit1_ne_zero _: โ_
#align nat.shiftl'_tt_ne_zero Nat.shiftl'_tt_ne_zero: โ (m : โ) {n : โ}, n โ  0 โ shiftl' true m n โ  0Nat.shiftl'_tt_ne_zero

/-! ### `size` -/

@[simp]
theorem size_zero: size 0 = 0size_zero : size: โ โ โsize 0: ?m.37340 = 0: ?m.37450 := byGoals accomplished! ๐ size 0 = 0simp [size: โ โ โsize]Goals accomplished! ๐
#align nat.size_zero Nat.size_zero: size 0 = 0Nat.size_zero

@[simp]
theorem size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit {b: Boolb n: ?m.3795n} (h: bit b n โ  0h : bit: Bool โ โ โ โbit b: ?m.3792b n: ?m.3795n โ  0: ?m.38010) : size: โ โ โsize (bit: Bool โ โ โ โbit b: ?m.3792b n: ?m.3795n) = succ: โ โ โsucc (size: โ โ โsize n: ?m.3795n) := byGoals accomplished! ๐
b: Booln: โh: bit b n โ  0size (bit b n) = succ (size n)rw [b: Booln: โh: bit b n โ  0size (bit b n) = succ (size n)size: โ โ โsizeb: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)]b: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
b: Booln: โh: bit b n โ  0size (bit b n) = succ (size n)conv =>b: Booln: โh: bit b n โ  0succ (binaryRec 0 (fun x x => succ) (div2 (bit b n)))
b: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)lhsb: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n)
b: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)rw [b: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n)binaryRec: {C : โ โ Sort ?u.4003} โ C 0 โ ((b : Bool) โ (n : โ) โ C n โ C (bit b n)) โ (n : โ) โ C nbinaryRecb: Booln: โh: bit b n โ  0if n0 : bit b n = 0 then Eq.mpr (_ : โ = โ) 0
else
let n' := div2 (bit b n);
let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
Eq.mpr (_ : โ = โ) (succ (binaryRec 0 (fun x x => succ) n'))]b: Booln: โh: bit b n โ  0if n0 : bit b n = 0 then Eq.mpr (_ : โ = โ) 0
else
let n' := div2 (bit b n);
let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
Eq.mpr (_ : โ = โ) (succ (binaryRec 0 (fun x x => succ) n'))
b: Booln: โh: bit b n โ  0binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)simp [h: bit b n โ  0h]b: Booln: โh: bit b n โ  0succ (binaryRec 0 (fun x x => succ) (div2 (bit b n)))
b: Booln: โh: bit b n โ  0size (bit b n) = succ (size n)rw [b: Booln: โh: bit b n โ  0succ (binaryRec 0 (fun x x => succ) (div2 (bit b n))) = succ (binaryRec 0 (fun x x => succ) n)div2_bit: โ (b : Bool) (n : โ), div2 (bit b n) = ndiv2_bitb: Booln: โh: bit b n โ  0succ (binaryRec 0 (fun x x => succ) n) = succ (binaryRec 0 (fun x x => succ) n)]Goals accomplished! ๐
#align nat.size_bit Nat.size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)Nat.size_bit

section
set_option linter.deprecated false

@[simp]
theorem size_bit0: โ {n : โ}, n โ  0 โ size (bit0 n) = succ (size n)size_bit0 {n: โn} (h: n โ  0h : n: ?m.4824n โ  0: ?m.48300) : size: โ โ โsize (bit0: {ฮฑ : Type ?u.4844} โ [inst : Add ฮฑ] โ ฮฑ โ ฮฑbit0 n: ?m.4824n) = succ: โ โ โsucc (size: โ โ โsize n: ?m.4824n) :=
@size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit false: Boolfalse n: โn (Nat.bit0_ne_zero: โ {n : โ}, n โ  0 โ bit0 n โ  0Nat.bit0_ne_zero h: n โ  0h)
#align nat.size_bit0 Nat.size_bit0: โ {n : โ}, n โ  0 โ size (bit0 n) = succ (size n)Nat.size_bit0

@[simp]
theorem size_bit1: โ (n : โ), size (bit1 n) = succ (size n)size_bit1 (n: ?m.4925n) : size: โ โ โsize (bit1: {ฮฑ : Type ?u.4929} โ [inst : One ฮฑ] โ [inst : Add ฮฑ] โ ฮฑ โ ฮฑbit1 n: ?m.4925n) = succ: โ โ โsucc (size: โ โ โsize n: ?m.4925n) :=
@size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit true: Booltrue n: โn (Nat.bit1_ne_zero: โ (n : โ), bit1 n โ  0Nat.bit1_ne_zero n: โn)
#align nat.size_bit1 Nat.size_bit1: โ (n : โ), size (bit1 n) = succ (size n)Nat.size_bit1

@[simp]
theorem size_one: size 1 = 1size_one : size: โ โ โsize 1: ?m.50431 = 1: ?m.50541 :=
show size: โ โ โsize (bit1: {ฮฑ : Type ?u.5073} โ [inst : One ฮฑ] โ [inst : Add ฮฑ] โ ฮฑ โ ฮฑbit1 0: ?m.51260) = 1: ?m.51571 by rw [size (bit1 0) = 1size_bit1: โ (n : โ), size (bit1 n) = succ (size n)size_bit1,succ (size 0) = 1 size (bit1 0) = 1size_zero: size 0 = 0size_zerosucc 0 = 1]Goals accomplished! ๐
#align nat.size_one Nat.size_one: size 1 = 1Nat.size_one

end

@[simp]
theorem size_shiftl': โ {b : Bool} {m n : โ}, shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nsize_shiftl' {b: Boolb m: โm n: ?m.5213n} (h: shiftl' b m n โ  0h : shiftl': Bool โ โ โ โ โ โshiftl' b: ?m.5207b m: ?m.5210m n: ?m.5213n โ  0: ?m.52190) : size: โ โ โsize (shiftl': Bool โ โ โ โ โ โshiftl' b: ?m.5207b m: ?m.5210m n: ?m.5213n) = size: โ โ โsize m: ?m.5210m + n: ?m.5213n := byGoals accomplished! ๐
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + ninduction' n: โn with n: โn IH: ?m.5293 nIHb: Boolm, n: โhโ: shiftl' b m n โ  0h: shiftl' b m zero โ  0zerosize (shiftl' b m zero) = size m + zerob: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: shiftl' b m (succ n) โ  0succsize (shiftl' b m (succ n)) = size m + succ n b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + n<;>b: Boolm, n: โhโ: shiftl' b m n โ  0h: shiftl' b m zero โ  0zerosize (shiftl' b m zero) = size m + zerob: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: shiftl' b m (succ n) โ  0succsize (shiftl' b m (succ n)) = size m + succ n b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nsimp [shiftl': Bool โ โ โ โ โ โshiftl'] at h: shiftl' b m zero โ  0hโขb: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsize (bit b (shiftl' b m n)) = size m + succ n
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nrw [b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsize (bit b (shiftl' b m n)) = size m + succ nsize_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit h: ยฌbit b (shiftl' b m n) = 0h,b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsucc (size (shiftl' b m n)) = size m + succ n b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsize (bit b (shiftl' b m n)) = size m + succ nNat.add_succ: โ (n m : โ), n + succ m = succ (n + m)Nat.add_succb: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsucc (size (shiftl' b m n)) = succ (size m + n)]b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsucc (size (shiftl' b m n)) = succ (size m + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nby_cases s0: ?m.5775s0 : shiftl': Bool โ โ โ โ โ โshiftl' b: Boolb m: โm n: โn = 0: ?m.57290b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: shiftl' b m n = 0possucc (size (shiftl' b m n)) = succ (size m + n)b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: ยฌshiftl' b m n = 0negsucc (size (shiftl' b m n)) = succ (size m + n) <;> [b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsucc (size (shiftl' b m n)) = succ (size m + n)skipb: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: shiftl' b m n = 0possucc (size (shiftl' b m n)) = succ (size m + n); b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0succsucc (size (shiftl' b m n)) = succ (size m + n)rw [b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: ยฌshiftl' b m n = 0negsucc (size (shiftl' b m n)) = succ (size m + n)IH: ?m.5293 nIH s0: ?m.5775s0b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: ยฌshiftl' b m n = 0negsucc (size m + n) = succ (size m + n)]Goals accomplished! ๐]b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: shiftl' b m n = 0possucc (size (shiftl' b m n)) = succ (size m + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nrw [b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b (shiftl' b m n) = 0s0: shiftl' b m n = 0possucc (size (shiftl' b m n)) = succ (size m + n)s0: shiftl' b m n = 0s0b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b 0 = 0s0: shiftl' b m n = 0possucc (size 0) = succ (size m + n)]b: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b 0 = 0s0: shiftl' b m n = 0possucc (size 0) = succ (size m + n) at h: ยฌbit b (shiftl' b m n) = 0hโขb: Boolm, nโ: โhโ: shiftl' b m nโ โ  0n: โIH: shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nh: ยฌbit b 0 = 0s0: shiftl' b m n = 0possucc (size 0) = succ (size m + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + ncases b: Boolbm, nโ, n: โhโ: shiftl' false m nโ โ  0IH: shiftl' false m n โ  0 โ size (shiftl' false m n) = size m + nh: ยฌbit false 0 = 0s0: shiftl' false m n = 0pos.falsesucc (size 0) = succ (size m + n)m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0pos.truesucc (size 0) = succ (size m + n);m, nโ, n: โhโ: shiftl' false m nโ โ  0IH: shiftl' false m n โ  0 โ size (shiftl' false m n) = size m + nh: ยฌbit false 0 = 0s0: shiftl' false m n = 0pos.falsesucc (size 0) = succ (size m + n)m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0pos.truesucc (size 0) = succ (size m + n) b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nยทm, nโ, n: โhโ: shiftl' false m nโ โ  0IH: shiftl' false m n โ  0 โ size (shiftl' false m n) = size m + nh: ยฌbit false 0 = 0s0: shiftl' false m n = 0pos.falsesucc (size 0) = succ (size m + n) m, nโ, n: โhโ: shiftl' false m nโ โ  0IH: shiftl' false m n โ  0 โ size (shiftl' false m n) = size m + nh: ยฌbit false 0 = 0s0: shiftl' false m n = 0pos.falsesucc (size 0) = succ (size m + n)m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0pos.truesucc (size 0) = succ (size m + n)exact absurd: โ {a : Prop} {b : Sort ?u.5887}, a โ ยฌa โ babsurd rfl: โ {ฮฑ : Sort ?u.5890} {a : ฮฑ}, a = arfl h: ยฌbit false 0 = 0hGoals accomplished! ๐
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nhave : shiftl': Bool โ โ โ โ โ โshiftl' true: Booltrue m: โm n: โn + 1: ?m.59151 = 1: ?m.59311 := congr_arg: โ {ฮฑ : Sort ?u.5998} {ฮฒ : Sort ?u.5997} {aโ aโ : ฮฑ} (f : ฮฑ โ ฮฒ), aโ = aโ โ f aโ = f aโcongr_arg (ยท + 1): โ โ โ(ยท + 1) s0: shiftl' true m n = 0s0m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0this: shiftl' true m n + 1 = 1pos.truesucc (size 0) = succ (size m + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nrw [m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0this: shiftl' true m n + 1 = 1pos.truesucc (size 0) = succ (size m + n)shiftl'_tt_eq_mul_pow: โ (m n : โ), shiftl' true m n + 1 = (m + 1) * 2 ^ nshiftl'_tt_eq_mul_powm, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0this: (m + 1) * 2 ^ n = 1pos.truesucc (size 0) = succ (size m + n)]m, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0this: (m + 1) * 2 ^ n = 1pos.truesucc (size 0) = succ (size m + n) at this: shiftl' true m n + 1 = 1thism, nโ, n: โhโ: shiftl' true m nโ โ  0IH: shiftl' true m n โ  0 โ size (shiftl' true m n) = size m + nh: ยฌbit true 0 = 0s0: shiftl' true m n = 0this: (m + 1) * 2 ^ n = 1pos.truesucc (size 0) = succ (size m + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nobtain rfl: m = 0rfl := succ.inj: โ {n n_1 : โ}, succ n = succ n_1 โ n = n_1succ.inj (eq_one_of_dvd_one: โ {n : โ}, n โฃ 1 โ n = 1eq_one_of_dvd_one โจ_: ?m.6136_, this: (m + 1) * 2 ^ n = 1this.symm: โ {ฮฑ : Sort ?u.6144} {a b : ฮฑ}, a = b โ b = asymmโฉ)nโ, n: โhโ: ยฌbit true 0 = 0h: shiftl' true 0 nโ โ  0IH: shiftl' true 0 n โ  0 โ size (shiftl' true 0 n) = size 0 + ns0: shiftl' true 0 n = 0this: (0 + 1) * 2 ^ n = 1pos.truesucc (size 0) = succ (size 0 + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nsimp only [zero_add: โ {M : Type ?u.6196} [inst : AddZeroClass M] (a : M), 0 + a = azero_add, one_mul: โ {M : Type ?u.6213} [inst : MulOneClass M] (a : M), 1 * a = aone_mul] at this: (0 + 1) * 2 ^ n = 1thisnโ, n: โhโ: ยฌbit true 0 = 0h: shiftl' true 0 nโ โ  0IH: shiftl' true 0 n โ  0 โ size (shiftl' true 0 n) = size 0 + ns0: shiftl' true 0 n = 0this: 2 ^ n = 1pos.truesucc (size 0) = succ (size 0 + n)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nobtain: n = 0obtain rfl: ?mโrfl : n: โn = 0: ?m.64080 :=
Nat.eq_zero_of_le_zero: โ {n : โ}, n โค 0 โ n = 0Nat.eq_zero_of_le_zero
(le_of_not_gt: โ {ฮฑ : Type ?u.6430} [inst : LinearOrder ฮฑ] {a b : ฮฑ}, ยฌa > b โ a โค ble_of_not_gt fun hn: ?m.6470hn => ne_of_gt: โ {a b : โ}, b < a โ a โ  bne_of_gt (pow_lt_pow_of_lt_right: โ {x : โ}, 1 < x โ โ {i j : โ}, i < j โ x ^ i < x ^ jpow_lt_pow_of_lt_right (nโ, n: โhโ: ยฌbit true 0 = 0h: shiftl' true 0 nโ โ  0IH: shiftl' true 0 n โ  0 โ size (shiftl' true 0 n) = size 0 + ns0: shiftl' true 0 n = 0this: 2 ^ n = 1pos.truesucc (size 0) = succ (size 0 + n)byGoals accomplished! ๐ nโ, n: โhโ: ยฌbit true 0 = 0h: shiftl' true 0 nโ โ  0IH: shiftl' true 0 n โ  0 โ size (shiftl' true 0 n) = size 0 + ns0: shiftl' true 0 n = 0this: 2 ^ n = 1hn: n > 01 < 2decideGoals accomplished! ๐) hn: ?m.6470hn) this: 2 ^ n = 1this)n: โhโ: ยฌbit true 0 = 0h: shiftl' true 0 n โ  0IH: shiftl' true 0 0 โ  0 โ size (shiftl' true 0 0) = size 0 + 0s0: shiftl' true 0 0 = 0this: 2 ^ 0 = 1pos.truesucc (size 0) = succ (size 0 + 0)
b: Boolm, n: โh: shiftl' b m n โ  0size (shiftl' b m n) = size m + nrflGoals accomplished! ๐
#align nat.size_shiftl' Nat.size_shiftl': โ {b : Bool} {m n : โ}, shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nNat.size_shiftl'

@[simp]
theorem size_shiftl: โ {m : โ}, m โ  0 โ โ (n : โ), size (shiftl m n) = size m + nsize_shiftl {m: โm} (h: m โ  0h : m: ?m.6632m โ  0: ?m.66380) (n: ?m.6651n) : size: โ โ โsize (shiftl: โ โ โ โ โshiftl m: ?m.6632m n: ?m.6651n) = size: โ โ โsize m: ?m.6632m + n: ?m.6651n :=
size_shiftl': โ {b : Bool} {m n : โ}, shiftl' b m n โ  0 โ size (shiftl' b m n) = size m + nsize_shiftl' (shiftl'_ne_zero_left: โ (b : Bool) {m : โ}, m โ  0 โ โ (n : โ), shiftl' b m n โ  0shiftl'_ne_zero_left _: Bool_ h: m โ  0h _: โ_)
#align nat.size_shiftl Nat.size_shiftl: โ {m : โ}, m โ  0 โ โ (n : โ), size (shiftl m n) = size m + nNat.size_shiftl

theorem lt_size_self: โ (n : โ), n < 2 ^ size nlt_size_self (n: โn : โ: Typeโ) : n: โn < 2: ?m.67562 ^ size: โ โ โsize n: โn := byGoals accomplished! ๐
n: โn < 2 ^ size nrw [n: โn < 2 ^ size nโ one_shiftl: โ (n : โ), shiftl 1 n = 2 ^ none_shiftln: โn < shiftl 1 (size n)]n: โn < shiftl 1 (size n)
n: โn < 2 ^ size nhave : โ {n: ?m.6842n}, n: ?m.6842n = 0: ?m.68480 โ n: ?m.6842n < shiftl: โ โ โ โ โshiftl 1: ?m.68731 (size: โ โ โsize n: ?m.6842n) := n: โn < shiftl 1 (size n)byGoals accomplished! ๐ n: โโ {n : โ}, n = 0 โ n < shiftl 1 (size n)simpGoals accomplished! ๐
n: โn < 2 ^ size napply binaryRec: โ {C : โ โ Sort ?u.7322}, C 0 โ (โ (b : Bool) (n : โ), C n โ C (bit b n)) โ โ (n : โ), C nbinaryRec _: ?m.7323 0_ _: โ (b : Bool) (n : โ), ?m.7323 n โ ?m.7323 (bit b n)_ n: โnn: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)0 < shiftl 1 (size 0)n: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)โ (b : Bool) (n : โ), n < shiftl 1 (size n) โ bit b n < shiftl 1 (size (bit b n))
n: โn < 2 ^ size nยทn: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)0 < shiftl 1 (size 0) n: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)0 < shiftl 1 (size 0)n: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)โ (b : Bool) (n : โ), n < shiftl 1 (size n) โ bit b n < shiftl 1 (size (bit b n))apply this: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)this rfl: โ {ฮฑ : Sort ?u.7331} {a : ฮฑ}, a = arflGoals accomplished! ๐
n: โn < 2 ^ size nintro b: Boolb n: โn IH: ?m.7323 nIHnโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)bit b n < shiftl 1 (size (bit b n))
n: โn < 2 ^ size nby_cases h: ?m.7384h : bit: Bool โ โ โ โbit b: Boolb n: โn = 0: ?m.73450nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: bit b n = 0posbit b n < shiftl 1 (size (bit b n))nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < shiftl 1 (size (bit b n))
n: โn < 2 ^ size nยทnโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: bit b n = 0posbit b n < shiftl 1 (size (bit b n)) nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: bit b n = 0posbit b n < shiftl 1 (size (bit b n))nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < shiftl 1 (size (bit b n))apply this: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)this h: ?m.7384hGoals accomplished! ๐
n: โn < 2 ^ size nrw [nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < shiftl 1 (size (bit b n))size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit h: ?m.7391h,nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < shiftl 1 (succ (size n)) nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < shiftl 1 (size (bit b n))shiftl_succ: โ (m n : โ), shiftl m (n + 1) = bit0 (shiftl m n)shiftl_succnโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < bit0 (shiftl 1 (size n))]nโ: โthis: โ {n : โ}, n = 0 โ n < shiftl 1 (size n)b: Booln: โIH: n < shiftl 1 (size n)h: ยฌbit b n = 0negbit b n < bit0 (shiftl 1 (size n))
n: โn < 2 ^ size nexact bit_lt_bit0: โ (b : Bool) {m n : โ}, m < n โ bit b m < bit0 nbit_lt_bit0 _: Bool_ IH: ?m.7323 nIHGoals accomplished! ๐
#align nat.lt_size_self Nat.lt_size_self: โ (n : โ), n < 2 ^ size nNat.lt_size_self

theorem size_le: โ {m n : โ}, size m โค n โ m < 2 ^ nsize_le {m: โm n: โn : โ: Typeโ} : size: โ โ โsize m: โm โค n: โn โ m: โm < 2: ?m.74692 ^ n: โn :=
โจfun h: ?m.7545h => lt_of_lt_of_le: โ {ฮฑ : Type ?u.7547} [inst : Preorder ฮฑ] {a b c : ฮฑ}, a < b โ b โค c โ a < clt_of_lt_of_le (lt_size_self: โ (n : โ), n < 2 ^ size nlt_size_self _: โ_) (pow_le_pow_of_le_right: โ {n : โ}, n > 0 โ โ {i j : โ}, i โค j โ n ^ i โค n ^ jpow_le_pow_of_le_right (byGoals accomplished! ๐ m, n: โh: size m โค n2 > 0decideGoals accomplished! ๐) h: ?m.7545h), byGoals accomplished! ๐
m, n: โm < 2 ^ n โ size m โค nrw [m, n: โm < 2 ^ n โ size m โค nโ one_shiftl: โ (n : โ), shiftl 1 n = 2 ^ none_shiftlm, n: โm < shiftl 1 n โ size m โค n]m, n: โm < shiftl 1 n โ size m โค n;m, n: โm < shiftl 1 n โ size m โค n m, n: โm < 2 ^ n โ size m โค nrevert n: โnm: โโ {n : โ}, m < shiftl 1 n โ size m โค n
m, n: โm < 2 ^ n โ size m โค napply binaryRec: โ {C : โ โ Sort ?u.7689}, C 0 โ (โ (b : Bool) (n : โ), C n โ C (bit b n)) โ โ (n : โ), C nbinaryRec _: ?m.7690 0_ _: โ (b : Bool) (n : โ), ?m.7690 n โ ?m.7690 (bit b n)_ m: โmm: โโ {n : โ}, 0 < shiftl 1 n โ size 0 โค nm: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1
m, n: โm < 2 ^ n โ size m โค nยทm: โโ {n : โ}, 0 < shiftl 1 n โ size 0 โค n m: โโ {n : โ}, 0 < shiftl 1 n โ size 0 โค nm: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1intro n: โnm, n: โ0 < shiftl 1 n โ size 0 โค n
m: โโ {n : โ}, 0 < shiftl 1 n โ size 0 โค nsimpGoals accomplished! ๐
m, n: โm < 2 ^ n โ size m โค nยทm: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1 m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1intro b: Boolb m: โm IH: ?m.7690 mIH n: โn h: bit b m < shiftl 1 nhmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 nsize (bit b m) โค n
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1by_cases e: ?m.8132e : bit: Bool โ โ โ โbit b: Boolb m: โm = 0: ?m.80930mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: bit b m = 0possize (bit b m) โค nmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: ยฌbit b m = 0negsize (bit b m) โค n
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1ยทmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: bit b m = 0possize (bit b m) โค n mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: bit b m = 0possize (bit b m) โค nmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: ยฌbit b m = 0negsize (bit b m) โค nsimp [e: ?m.8132e]Goals accomplished! ๐
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1rw [mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: ยฌbit b m = 0negsize (bit b m) โค nsize_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit e: ?m.8139emโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: ยฌbit b m = 0negsucc (size m) โค n]mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค nn: โh: bit b m < shiftl 1 ne: ยฌbit b m = 0negsucc (size m) โค n
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1cases' n: โn with n: โnmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0h: bit b m < shiftl 1 zeroneg.zerosucc (size m) โค zeromโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)neg.succsucc (size m) โค succ n
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1ยทmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0h: bit b m < shiftl 1 zeroneg.zerosucc (size m) โค zero mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0h: bit b m < shiftl 1 zeroneg.zerosucc (size m) โค zeromโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)neg.succsucc (size m) โค succ nexact e: ?m.8139e.elim: โ {a : Prop} {ฮฑ : Sort ?u.8385}, ยฌa โ a โ ฮฑelim (Nat.eq_zero_of_le_zero: โ {n : โ}, n โค 0 โ n = 0Nat.eq_zero_of_le_zero (le_of_lt_succ: โ {m n : โ}, m < succ n โ m โค nle_of_lt_succ h: bit b m < shiftl 1 zeroh))Goals accomplished! ๐
m: โโ (b : Bool) (n : โ),
(โ {n_1 : โ}, n < shiftl 1 n_1 โ size n โค n_1) โ โ {n_1 : โ}, bit b n < shiftl 1 n_1 โ size (bit b n) โค n_1ยทmโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)neg.succsucc (size m) โค succ n mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)neg.succsucc (size m) โค succ napply succ_le_succ: โ {n m : โ}, n โค m โ succ n โค succ msucc_le_succ (IH: ?m.7690 mIH _: m < shiftl 1 ?m.8411_)mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)m < shiftl 1 n
mโ: โb: Boolm: โIH: โ {n : โ}, m < shiftl 1 n โ size m โค ne: ยฌbit b m = 0n: โh: bit b m < shiftl 1 (succ n)neg.succsucc (size m) โค succ napply lt_imp_lt_of_le_imp_le: โ {ฮฑ : Type ?u.8413} {ฮฒ : Type ?u.8414} [inst : LinearOrder ฮฑ] [inst_1 : Preorder ฮฒ] {a b : ฮฑ} {c d : ฮฒ},
(a โค b โ c โค d) โ d < c โ b < alt_imp_lt_of_le_imp_le (fun h': ?m.8424h' => bit0_le_bit: โ (b : Bool) {m n : โ}, m โค n โ bit0 m โค bit b nbit0_le_bit _: Bool_ h': ?m.8424h') h: bit b m < shiftl 1 (succ n)hGoals accomplished! ๐โฉ
#align nat.size_le Nat.size_le: โ {m n : โ}, size m โค n โ m < 2 ^ nNat.size_le

theorem lt_size: โ {m n : โ}, m < size n โ 2 ^ m โค nlt_size {m: โm n: โn : โ: Typeโ} : m: โm < size: โ โ โsize n: โn โ 2: ?m.85722 ^ m: โm โค n: โn := byGoals accomplished! ๐
m, n: โm < size n โ 2 ^ m โค nrw [m, n: โm < size n โ 2 ^ m โค nโ not_lt: โ {ฮฑ : Type ?u.8645} [inst : LinearOrder ฮฑ] {a b : ฮฑ}, ยฌa < b โ b โค anot_lt,m, n: โm < size n โ ยฌn < 2 ^ m m, n: โm < size n โ 2 ^ m โค nDecidable.iff_not_comm: โ {a b : Prop} [inst : Decidable a] [inst : Decidable b], (a โ ยฌb) โ (b โ ยฌa)Decidable.iff_not_comm,m, n: โn < 2 ^ m โ ยฌm < size n m, n: โm < size n โ 2 ^ m โค nnot_lt: โ {ฮฑ : Type ?u.9190} [inst : LinearOrder ฮฑ] {a b : ฮฑ}, ยฌa < b โ b โค anot_lt,m, n: โn < 2 ^ m โ size n โค m m, n: โm < size n โ 2 ^ m โค nsize_le: โ {m n : โ}, size m โค n โ m < 2 ^ nsize_lem, n: โn < 2 ^ m โ n < 2 ^ m]Goals accomplished! ๐
#align nat.lt_size Nat.lt_size: โ {m n : โ}, m < size n โ 2 ^ m โค nNat.lt_size

theorem size_pos: โ {n : โ}, 0 < size n โ 0 < nsize_pos {n: โn : โ: Typeโ} : 0: ?m.92660 < size: โ โ โsize n: โn โ 0: ?m.93010 < n: โn := byGoals accomplished! ๐ n: โ0 < size n โ 0 < nrw [n: โ0 < size n โ 0 < nlt_size: โ {m n : โ}, m < size n โ 2 ^ m โค nlt_sizen: โ2 ^ 0 โค n โ 0 < n]n: โ2 ^ 0 โค n โ 0 < n;n: โ2 ^ 0 โค n โ 0 < n n: โ0 < size n โ 0 < nrflGoals accomplished! ๐
#align nat.size_pos Nat.size_pos: โ {n : โ}, 0 < size n โ 0 < nNat.size_pos

theorem size_eq_zero: โ {n : โ}, size n = 0 โ n = 0size_eq_zero {n: โn : โ: Typeโ} : size: โ โ โsize n: โn = 0: ?m.93710 โ n: โn = 0: ?m.93970 := byGoals accomplished! ๐
n: โsize n = 0 โ n = 0have := @size_pos: โ {n : โ}, 0 < size n โ 0 < nsize_pos n: โnn: โthis: 0 < size n โ 0 < nsize n = 0 โ n = 0;n: โthis: 0 < size n โ 0 < nsize n = 0 โ n = 0 n: โsize n = 0 โ n = 0simp [pos_iff_ne_zero: โ {ฮฑ : Type ?u.9423} [inst : CanonicallyOrderedAddMonoid ฮฑ] {a : ฮฑ}, 0 < a โ a โ  0pos_iff_ne_zero] at this: ?m.9418thisn: โthis: ยฌsize n = 0 โ ยฌn = 0size n = 0 โ n = 0;n: โthis: ยฌsize n = 0 โ ยฌn = 0size n = 0 โ n = 0 n: โsize n = 0 โ n = 0exact Decidable.not_iff_not: โ {a b : Prop} [inst : Decidable a] [inst : Decidable b], (ยฌa โ ยฌb) โ (a โ b)Decidable.not_iff_not.1: โ {a b : Prop}, (a โ b) โ a โ b1 this: ยฌsize n = 0 โ ยฌn = 0thisGoals accomplished! ๐
#align nat.size_eq_zero Nat.size_eq_zero: โ {n : โ}, size n = 0 โ n = 0Nat.size_eq_zero

theorem size_pow: โ {n : โ}, size (2 ^ n) = n + 1size_pow {n: โn : โ: Typeโ} : size: โ โ โsize (2: ?m.100382 ^ n: โn) = n: โn + 1: ?m.101011 :=
le_antisymm: โ {ฮฑ : Type ?u.10160} [inst : PartialOrder ฮฑ] {a b : ฮฑ}, a โค b โ b โค a โ a = ble_antisymm (size_le: โ {m n : โ}, size m โค n โ m < 2 ^ nsize_le.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| pow_lt_pow_of_lt_right: โ {x : โ}, 1 < x โ โ {i j : โ}, i < j โ x ^ i < x ^ jpow_lt_pow_of_lt_right (byGoals accomplished! ๐ n: โ1 < 2decideGoals accomplished! ๐) (lt_succ_self: โ (n : โ), n < succ nlt_succ_self _: โ_))
(lt_size: โ {m n : โ}, m < size n โ 2 ^ m โค nlt_size.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| le_rfl: โ {ฮฑ : Type ?u.10276} [inst : Preorder ฮฑ] {a : ฮฑ}, a โค ale_rfl)
#align nat.size_pow Nat.size_pow: โ {n : โ}, size (2 ^ n) = n + 1Nat.size_pow

theorem size_le_size: โ {m n : โ}, m โค n โ size m โค size nsize_le_size {m: โm n: โn : โ: Typeโ} (h: m โค nh : m: โm โค n: โn) : size: โ โ โsize m: โm โค size: โ โ โsize n: โn :=
size_le: โ {m n : โ}, size m โค n โ m < 2 ^ nsize_le.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| lt_of_le_of_lt: โ {ฮฑ : Type ?u.10397} [inst : Preorder ฮฑ] {a b c : ฮฑ}, a โค b โ b < c โ a < clt_of_le_of_lt h: m โค nh (lt_size_self: โ (n : โ), n < 2 ^ size nlt_size_self _: โ_)
#align nat.size_le_size Nat.size_le_size: โ {m n : โ}, m โค n โ size m โค size nNat.size_le_size

theorem size_eq_bits_len: โ (n : โ), List.length (bits n) = size nsize_eq_bits_len (n: โn : โ: Typeโ) : n: โn.bits: โ โ List Boolbits.length: {ฮฑ : Type ?u.10482} โ List ฮฑ โ โlength = n: โn.size: โ โ โsize := byGoals accomplished! ๐
n: โList.length (bits n) = size ninduction' n: โn using Nat.binaryRec': {C : โ โ Sort u_1} โ C 0 โ ((b : Bool) โ (n : โ) โ (n = 0 โ b = true) โ C n โ C (bit b n)) โ (n : โ) โ C nNat.binaryRec' with b: Boolb n: โn h: n = 0 โ b = trueh ih: ?m.10507 nihzList.length (bits 0) = size 0b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = size (bit b n);zList.length (bits 0) = size 0b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = size (bit b n) n: โList.length (bits n) = size nยทzList.length (bits 0) = size 0 zList.length (bits 0) = size 0b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = size (bit b n)simpGoals accomplished! ๐
n: โList.length (bits n) = size nrw [b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = size (bit b n)size_bit: โ {b : Bool} {n : โ}, bit b n โ  0 โ size (bit b n) = succ (size n)size_bit,b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = succ (size n)b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0 b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (bits (bit b n)) = size (bit b n)bits_append_bit: โ (n : โ) (b : Bool), (n = 0 โ b = true) โ bits (bit b n) = b :: bits nbits_append_bit _: โ_ _: Bool_ h: n = 0 โ b = truehb: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (b :: bits n) = succ (size n)b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0]b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (b :: bits n) = succ (size n)b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0
n: โList.length (bits n) = size nยทb: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (b :: bits n) = succ (size n) b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfList.length (b :: bits n) = succ (size n)b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0simp [ih: ?m.10507 nih]Goals accomplished! ๐
n: โList.length (bits n) = size nยทb: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0 b: Booln: โh: n = 0 โ b = trueih: List.length (bits n) = size nfbit b n โ  0simpa [bit_eq_zero_iff: โ {n : โ} {b : Bool}, bit b n = 0 โ n = 0 โง b = falsebit_eq_zero_iff]Goals accomplished! ๐
#align nat.size_eq_bits_len Nat.size_eq_bits_len: โ (n : โ), List.length (bits n) = size nNat.size_eq_bits_len

end Nat
```