case zero
α : Type ?u.621708
n : ℕ
⊢ ↑0 = Nat.shiftl (↑zero) n

case pos
α : Type ?u.621708
n : ℕ
a✝ : PosNum
⊢ ↑(pos (PosNum.shiftl a✝ n)) = Nat.shiftl (↑(pos a✝)) n
α : Type ?u.621708
m : Num
n : ℕ
⊢ ↑(shiftl m n) = Nat.shiftl (↑m) n
cases m <;> dsimp only [shiftl]
case pos
α : Type ?u.621708
n : ℕ
a✝ : PosNum
⊢ ↑(PosNum.shiftl a✝ n) = Nat.shiftl (↑a✝) n
case pos
α : Type ?u.621708
n : ℕ
a✝ : PosNum
⊢ ↑(pos (PosNum.shiftl a✝ n)) = Nat.shiftl (↑(pos a✝)) n
simp only [cast_pos]
case pos.zero
α : Type ?u.621708
a✝ : PosNum
⊢ ↑(PosNum.shiftl a✝ Nat.zero) = Nat.shiftl (↑a✝) Nat.zero

case pos.succ
α : Type ?u.621708
a✝ : PosNum
n : ℕ
IH : ↑(PosNum.shiftl a✝ n) = Nat.shiftl (↑a✝) n
⊢ ↑(PosNum.shiftl a✝ (Nat.succ n)) = Nat.shiftl (↑a✝) (Nat.succ n)
case pos
α : Type ?u.621708
n : ℕ
a✝ : PosNum
⊢ ↑(PosNum.shiftl a✝ n) = Nat.shiftl (↑a✝) n
induction' n with n IH
no goals
case pos.succ
α : Type ?u.621708
a✝ : PosNum
n : ℕ
IH : ↑(PosNum.shiftl a✝ n) = Nat.shiftl (↑a✝) n
⊢ ↑(PosNum.shiftl a✝ (Nat.succ n)) = Nat.shiftl (↑a✝) (Nat.succ n)
simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftl_succ, IH]
case zero
α : Type ?u.621708
n : ℕ
⊢ Nat.shiftl (↑zero) n = ↑0
case zero
α : Type ?u.621708
n : ℕ
⊢ ↑0 = Nat.shiftl (↑zero) n
symm
no goals
case zero
α : Type ?u.621708
n : ℕ
⊢ Nat.shiftl (↑zero) n = ↑0
apply Nat.zero_shiftl
no goals
case pos.zero
α : Type ?u.621708
a✝ : PosNum
⊢ ↑(PosNum.shiftl a✝ Nat.zero) = Nat.shiftl (↑a✝) Nat.zero
rfl