case zero
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd (Nat.shiftr (↑zero) n)

case pos
α : Type ?u.633818
n : ℕ
a✝ : PosNum
⊢ PosNum.testBit a✝ n = Nat.bodd (Nat.shiftr (↑(pos a✝)) n)
α : Type ?u.633818
m : Num
n : ℕ
⊢ testBit m n = Nat.testBit (↑m) n
cases m <;> dsimp only [testBit, Nat.testBit]
case pos
α : Type ?u.633818
n : ℕ
a✝ : PosNum
⊢ PosNum.testBit a✝ n = Nat.bodd (Nat.shiftr (↑(pos a✝)) n)
case zero
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd (Nat.shiftr (↑zero) n)

case pos
α : Type ?u.633818
n : ℕ
a✝ : PosNum
⊢ PosNum.testBit a✝ n = Nat.bodd (Nat.shiftr (↑(pos a✝)) n)
case zero =>
  change false = Nat.bodd (Nat.shiftr 0 n)
  rw [Nat.zero_shiftr]
  rfl
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd (Nat.shiftr 0 n)
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd (Nat.shiftr (↑zero) n)
change false = Nat.bodd (Nat.shiftr 0 n)
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd 0
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd (Nat.shiftr 0 n)
rw [Nat.zero_shiftr]
no goals
α : Type ?u.633818
n : ℕ
⊢ false = Nat.bodd 0
rfl
case zero.one
α : Type ?u.633818
m : PosNum
⊢ true = Nat.bodd (Nat.shiftr (↑(pos one)) Nat.zero)

case zero.bit1
α : Type ?u.633818
m✝ m : PosNum
⊢ true = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit1 m))) Nat.zero)

case zero.bit0
α : Type ?u.633818
m✝ m : PosNum
⊢ false = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit0 m))) Nat.zero)

case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr (↑(pos one)) (Nat.succ n))

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

case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n))
α : Type ?u.633818
n : ℕ
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
induction' n with n IH generalizing m <;> cases' m with m m <;> dsimp only [PosNum.testBit]
no goals
case zero.one
α : Type ?u.633818
m : PosNum
⊢ true = Nat.bodd (Nat.shiftr (↑(pos one)) Nat.zero)
rfl
no goals
case zero.bit1
α : Type ?u.633818
m✝ m : PosNum
⊢ true = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit1 m))) Nat.zero)
exact (Nat.bodd_bit _ _).symm
no goals
case zero.bit0
α : Type ?u.633818
m✝ m : PosNum
⊢ false = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit0 m))) Nat.zero)
exact (Nat.bodd_bit _ _).symm
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr 1 (n + 1))
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr (↑(pos one)) (Nat.succ n))
change false = Nat.bodd (Nat.shiftr 1 (n + 1))
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr (Nat.shiftr 1 1) n)
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr 1 (n + 1))
rw [add_comm, Nat.shiftr_add]
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr 0 n)
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr (Nat.shiftr 1 1) n)
change false = Nat.bodd (Nat.shiftr 0 n)
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd 0
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd (Nat.shiftr 0 n)
rw [Nat.zero_shiftr]
no goals
case succ.one
α : Type ?u.633818
m : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
⊢ false = Nat.bodd 0
rfl
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit true ↑m) (n + 1))
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit1 m))) (Nat.succ n))
change PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit true m) (n + 1))
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.shiftr (Nat.bit true ↑m) 1) n)
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit true ↑m) (n + 1))
rw [add_comm, Nat.shiftr_add]
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.div2 (Nat.bit true ↑m)) n)
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.shiftr (Nat.bit true ↑m) 1) n)
dsimp only [Nat.shiftr]
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑m) n)
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.div2 (Nat.bit true ↑m)) n)
rw [Nat.div2_bit]
no goals
case succ.bit1
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑m) n)
apply IH
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit false ↑m) (n + 1))
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos (PosNum.bit0 m))) (Nat.succ n))
change PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit false m) (n + 1))
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.shiftr (Nat.bit false ↑m) 1) n)
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit false ↑m) (n + 1))
rw [add_comm, Nat.shiftr_add]
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.div2 (Nat.bit false ↑m)) n)
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.shiftr (Nat.bit false ↑m) 1) n)
dsimp only [Nat.shiftr]
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑m) n)
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.div2 (Nat.bit false ↑m)) n)
rw [Nat.div2_bit]
no goals
case succ.bit0
α : Type ?u.633818
m✝ : PosNum
n : ℕ
IH : ∀ (m : PosNum), PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑(pos m)) n)
m : PosNum
⊢ PosNum.testBit m n = Nat.bodd (Nat.shiftr (↑m) n)
apply IH