-- Mathlib/Data/Nat/Size.lean
theorem size_shiftLeft' {b m n} (h : shiftLeft' b m n ≠ 0) :
    size (shiftLeft' b m n) = size m + n

Proof state:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
rw [s0] at h ⊢

Result:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b 0 = 0
s0 : shiftLeft' b m n = 0
⊢ (size 0).succ = (m.size + n).succ

Proof state:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
by_cases s0 : shiftLeft' b m n = 0

Result:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

case neg
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Proof state:
case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ (size 0).succ = (size 0 + n).succ

Tactic:
simp only [zero_add, one_mul] at this

Result:
case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : 2 ^ n = 1
⊢ (size 0).succ = (size 0 + n).succ

Proof state:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b 0 = 0
s0 : shiftLeft' b m n = 0
⊢ (size 0).succ = (m.size + n).succ

Tactic:
cases b

Result:
case pos.false
m n : ℕ
IH : shiftLeft' false m n ≠ 0 → (shiftLeft' false m n).size = m.size + n
h : ¬bit false 0 = 0
s0 : shiftLeft' false m n = 0
⊢ (size 0).succ = (m.size + n).succ

case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
⊢ (size 0).succ = (m.size + n).succ

Proof state:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : shiftLeft' b m (n + 1) ≠ 0
⊢ (shiftLeft' b m (n + 1)).size = m.size + (n + 1)

Tactic:
simp only [shiftLeft', ne_eq] at h ⊢

Result:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (bit b (shiftLeft' b m n)).size = m.size + (n + 1)

Proof state:
case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : 2 ^ n = 1
⊢ (size 0).succ = (size 0 + n).succ

Tactic:
obtain rfl : n = 0 := not_ne_iff.1 fun hn ↦ ne_of_gt (Nat.one_lt_pow hn (by decide)) this

Result:
case pos.true
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 0 ≠ 0 → (shiftLeft' true 0 0).size = size 0 + 0
s0 : shiftLeft' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ (size 0).succ = (size 0 + 0).succ

Proof state:
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
rw [IH s0]

Result:
no goals

Proof state:
case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : shiftLeft' true m n + 1 = 1
⊢ (size 0).succ = (m.size + n).succ

Tactic:
rw [shiftLeft'_tt_eq_mul_pow] at this

Result:
case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ (size 0).succ = (m.size + n).succ

Proof state:
case pos.false
m n : ℕ
IH : shiftLeft' false m n ≠ 0 → (shiftLeft' false m n).size = m.size + n
h : ¬bit false 0 = 0
s0 : shiftLeft' false m n = 0
⊢ (size 0).succ = (m.size + n).succ

Tactic:
exact absurd rfl h

Result:
no goals

Proof state:
case zero
b : Bool
m : ℕ
h : shiftLeft' b m 0 ≠ 0
⊢ (shiftLeft' b m 0).size = m.size + 0

Tactic:
simp [shiftLeft']

Result:
no goals

Proof state:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (bit b (shiftLeft' b m n)).size = m.size + (n + 1)

Tactic:
rw [size_bit h, Nat.add_succ]

Result:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Proof state:
case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ (size 0).succ = (m.size + n).succ

Tactic:
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)

Result:
case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ (size 0).succ = (size 0 + n).succ

Proof state:
case pos.true
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 0 ≠ 0 → (shiftLeft' true 0 0).size = size 0 + 0
s0 : shiftLeft' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ (size 0).succ = (size 0 + 0).succ

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : 2 ^ n = 1
hn : n ≠ 0
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

case neg
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
case neg => rw [IH s0]

Result:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ