case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ size (bit b (shiftl' b m n)) = size m + succ n
b : Bool
m n : ℕ
h : shiftl' b m n ≠ 0
⊢ size (shiftl' b m n) = size m + n
induction' n with n IH <;> simp [shiftl'] at h⊢
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ size (bit b (shiftl' b m n)) = size m + succ n
rw [size_bit h, Nat.add_succ]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
by_cases s0 : shiftl' b m n = 0 <;> [skip; rw [IH s0]]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b 0 = 0
s0 : shiftl' b m n = 0
⊢ succ (size 0) = succ (size m + n)
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
rw [s0] at h⊢
case pos.false
m n✝ n : ℕ
h✝ : shiftl' false m n✝ ≠ 0
IH : shiftl' false m n ≠ 0 → size (shiftl' false m n) = size m + n
h : ¬bit false 0 = 0
s0 : shiftl' false m n = 0
⊢ succ (size 0) = succ (size m + n)

case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
⊢ succ (size 0) = succ (size m + n)
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b 0 = 0
s0 : shiftl' b m n = 0
⊢ succ (size 0) = succ (size m + n)
cases b
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size m + n)
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : shiftl' true m n + 1 = 1
⊢ succ (size 0) = succ (size m + n)
rw [shiftl'_tt_eq_mul_pow] at this
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size m + n)
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
simp only [zero_add, one_mul] at this
case pos.true
n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n ≠ 0
IH : shiftl' true 0 0 ≠ 0 → size (shiftl' true 0 0) = size 0 + 0
s0 : shiftl' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ succ (size 0) = succ (size 0 + 0)
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
obtain rfl : n = 0 :=
  Nat.eq_zero_of_le_zero
    (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_of_lt_right (by decide) hn) this)
no goals
case pos.true
n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n ≠ 0
IH : shiftl' true 0 0 ≠ 0 → size (shiftl' true 0 0) = size 0 + 0
s0 : shiftl' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ succ (size 0) = succ (size 0 + 0)
rfl
no goals
case pos.false
m n✝ n : ℕ
h✝ : shiftl' false m n✝ ≠ 0
IH : shiftl' false m n ≠ 0 → size (shiftl' false m n) = size m + n
h : ¬bit false 0 = 0
s0 : shiftl' false m n = 0
⊢ succ (size 0) = succ (size m + n)
exact absurd rfl h
no goals
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
hn : n > 0
⊢ 1 < 2
decide