[GOAL]
α : Type u_1
x✝ : Bool × ℕ
b : Bool
n : ℕ
⊢ boddDiv2 (uncurry bit (b, n)) = (b, n)
[PROOFSTEP]
simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
[GOAL]
α : Type u_1
n : ℕ
⊢ uncurry bit (boddDiv2 n) = n
[PROOFSTEP]
simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]
[GOAL]
α : Type u_1
⊢ ↑natSumNatEquivNat = Sum.elim bit0 bit1
[PROOFSTEP]
ext (x | x)
[GOAL]
case h.inl
α : Type u_1
x : ℕ
⊢ ↑natSumNatEquivNat (Sum.inl x) = Sum.elim bit0 bit1 (Sum.inl x)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
x : ℕ
⊢ ↑natSumNatEquivNat (Sum.inr x) = Sum.elim bit0 bit1 (Sum.inr x)
[PROOFSTEP]
rfl
