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

case pos
α : Type ?u.624959
n : ℕ
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
α : Type ?u.624959
m : Num
n : ℕ
⊢ ↑(shiftr m n) = Nat.shiftr (↑m) n
cases' m with m <;> dsimp only [shiftr]
case pos.zero
α : Type ?u.624959
m✝ m : PosNum
⊢ ↑(PosNum.shiftr m Nat.zero) = Nat.shiftr (↑(pos m)) Nat.zero

case pos.succ
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m (Nat.succ n)) = Nat.shiftr (↑(pos m)) (Nat.succ n)
case pos
α : Type ?u.624959
n : ℕ
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
induction' n with n IH generalizing m
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑0 = Nat.shiftr (↑(pos one)) (Nat.succ n)

case pos.succ.bit1
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)

case pos.succ.bit0
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)
case pos.succ
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m (Nat.succ n)) = Nat.shiftr (↑(pos m)) (Nat.succ n)
cases' m with m m <;> dsimp only [PosNum.shiftr]
case zero
α : Type ?u.624959
n : ℕ
⊢ Nat.shiftr (↑zero) n = ↑0
case zero
α : Type ?u.624959
n : ℕ
⊢ ↑0 = Nat.shiftr (↑zero) n
symm
no goals
case zero
α : Type ?u.624959
n : ℕ
⊢ Nat.shiftr (↑zero) n = ↑0
apply Nat.zero_shiftr
no goals
case pos.zero
α : Type ?u.624959
m✝ m : PosNum
⊢ ↑(PosNum.shiftr m Nat.zero) = Nat.shiftr (↑(pos m)) Nat.zero
cases m <;> rfl
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑0 = ↑(pos one) / 2 ^ Nat.succ n
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑0 = Nat.shiftr (↑(pos one)) (Nat.succ n)
rw [Nat.shiftr_eq_div_pow]
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑(pos one) / 2 ^ Nat.succ n = ↑0
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑0 = ↑(pos one) / 2 ^ Nat.succ n
symm
case pos.succ.one.h₀
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑(pos one) < 2 ^ Nat.succ n
case pos.succ.one
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑(pos one) / 2 ^ Nat.succ n = ↑0
apply Nat.div_eq_of_lt
no goals
case pos.succ.one.h₀
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ ↑(pos one) < 2 ^ Nat.succ n
exact @Nat.pow_lt_pow_of_lt_right 2 (by decide) 0 (n + 1) (Nat.succ_pos _)
no goals
α : Type ?u.624959
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
⊢ 1 < 2
decide
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = ?m.628320

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ?m.628320 = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ℕ
case pos.succ.bit1
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)
trans
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑(pos m)) n = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = ?m.628320

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ?m.628320 = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ℕ
apply IH
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (_root_.bit1 ↑m) (n + 1)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑(pos m)) n = Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n)
change Nat.shiftr m n = Nat.shiftr (_root_.bit1 m) (n + 1)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (Nat.shiftr (_root_.bit1 ↑m) 1) n
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (_root_.bit1 ↑m) (n + 1)
rw [add_comm n 1, Nat.shiftr_add]
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.shiftr (_root_.bit1 ↑m) 1
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (Nat.shiftr (_root_.bit1 ↑m) 1) n
apply congr_arg fun x => Nat.shiftr x n
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit1 ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.shiftr (_root_.bit1 ↑m) 1
repeat unfold Nat.shiftr
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (Nat.bit true ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit1 ↑m)
change (m : ℕ) = Nat.div2 (Nat.bit true m)
no goals
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (Nat.bit true ↑m)
rw [Nat.div2_bit]
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit1 ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit1 ↑m)
unfold Nat.shiftr
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = ?m.631988

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ?m.631988 = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ℕ
case pos.succ.bit0
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)
trans
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑(pos m)) n = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑(PosNum.shiftr m n) = ?m.631988

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ?m.631988 = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)

α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ℕ
apply IH
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (_root_.bit0 ↑m) (n + 1)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑(pos m)) n = Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n)
change Nat.shiftr m n = Nat.shiftr (_root_.bit0 m) (n + 1)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (Nat.shiftr (_root_.bit0 ↑m) 1) n
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (_root_.bit0 ↑m) (n + 1)
rw [add_comm n 1, Nat.shiftr_add]
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.shiftr (_root_.bit0 ↑m) 1
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ Nat.shiftr (↑m) n = Nat.shiftr (Nat.shiftr (_root_.bit0 ↑m) 1) n
apply congr_arg fun x => Nat.shiftr x n
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit0 ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.shiftr (_root_.bit0 ↑m) 1
repeat unfold Nat.shiftr
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (Nat.bit false ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit0 ↑m)
change (m : ℕ) = Nat.div2 (Nat.bit false m)
no goals
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (Nat.bit false ↑m)
rw [Nat.div2_bit]
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit0 ↑m)
α : Type ?u.624959
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), ↑(PosNum.shiftr m n) = Nat.shiftr (↑(pos m)) n
m : PosNum
⊢ ↑m = Nat.div2 (_root_.bit0 ↑m)
unfold Nat.shiftr