Theorem: Nat.size_le_self (Lib.lean)

State before:
n : ℕ
⊢ size n ≤ n
Tactic:
induction n using Nat.binaryRec' with
| z => exact le_refl _
| f b n hb ih =>
  rw [size_bit]
  cases b
  simp
  apply Nat.add_le_add (c := 1) ih
  { cases n
    exact absurd (hb rfl) Bool.noConfusion
    exact Nat.succ_le_succ (Nat.zero_le _) }
  simp
  apply Nat.succ_le_succ
  apply le_trans
  apply ih
  apply le_add_left
  cases b
  simpa using λ h ↦ absurd (hb h) Bool.noConfusion
  simp
State after:
no goals

State before:
case z

⊢ size 0 ≤ 0
Tactic:
exact le_refl _
State after:
no goals

State before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ size (bit b n) ≤ bit b n
Tactic:
rw [size_bit]
State after:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ succ (size n) ≤ bit b n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ succ (size n) ≤ bit b n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
cases b
State after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ bit false n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ bit false n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
simp
State after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ n + n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ n + n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply Nat.add_le_add (c := 1) ih
State after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
{ cases n
  exact absurd (hb rfl) Bool.noConfusion
  exact Nat.succ_le_succ (Nat.zero_le _) }
State after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
simp
State after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ n + n + 1

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ n + n + 1

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply Nat.succ_le_succ
State after:
case f.true.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.true.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply le_trans
State after:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ ?f.true.a.b

case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ?f.true.a.b ≤ n + n

case f.true.a.b
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ℕ

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ ?f.true.a.b

case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ?f.true.a.b ≤ n + n

case f.true.a.b
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ℕ

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply ih
State after:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply le_add_left
State after:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0

State before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
cases b
State after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ bit false n ≠ 0

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0

State before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ bit false n ≠ 0

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0
Tactic:
simpa using λ h ↦ absurd (hb h) Bool.noConfusion
State after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0

State before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0
Tactic:
simp
State after:
no goals

State before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n
Tactic:
cases n
State after:
case f.false.zero
ih : size zero ≤ zero
hb : zero = 0 → false = true
⊢ 1 ≤ zero

case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝

State before:
case f.false.zero
ih : size zero ≤ zero
hb : zero = 0 → false = true
⊢ 1 ≤ zero

case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Tactic:
exact absurd (hb rfl) Bool.noConfusion
State after:
case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝

State before:
case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Tactic:
exact Nat.succ_le_succ (Nat.zero_le _)
State after:
no goals