[GOAL]
α : Type u
e : Encoding α
⊢ Function.Injective e.encode
[PROOFSTEP]
refine' fun _ _ h => Option.some_injective _ _
[GOAL]
α : Type u
e : Encoding α
x✝¹ x✝ : α
h : encode e x✝¹ = encode e x✝
⊢ some x✝¹ = some x✝
[PROOFSTEP]
rw [← e.decode_encode, ← e.decode_encode, h]
[GOAL]
⊢ Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Γ'),
    x ∈
      { val := {blank, bit true, bit false, bra, ket, comma},
        nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
intro
[GOAL]
x✝ : Γ'
⊢ x✝ ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
cases_type* Γ' Bool
[GOAL]
case blank
⊢ blank ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bit.false
⊢ bit false ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bit.true
⊢ bit true ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bra
⊢ bra ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case ket
⊢ ket ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case comma
⊢ comma ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (n : PosNum), decodePosNum (encodePosNum n) = n
[PROOFSTEP]
intro n
[GOAL]
n : PosNum
⊢ decodePosNum (encodePosNum n) = n
[PROOFSTEP]
induction' n with m hm m hm
[GOAL]
case one
⊢ decodePosNum (encodePosNum PosNum.one) = PosNum.one
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ decodePosNum (encodePosNum (PosNum.bit1 m)) = PosNum.bit1 m
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ decodePosNum (encodePosNum (PosNum.bit0 m)) = PosNum.bit0 m
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case one
⊢ (if [] = [] then PosNum.one else PosNum.bit1 (decodePosNum [])) = PosNum.one
[PROOFSTEP]
rfl
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 (decodePosNum (encodePosNum m))) = PosNum.bit1 m
[PROOFSTEP]
rw [hm]
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 m) = PosNum.bit1 m
[PROOFSTEP]
exact if_neg (encodePosNum_nonempty m)
[GOAL]
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ PosNum.bit0 (decodePosNum (encodePosNum m)) = PosNum.bit0 m
[PROOFSTEP]
exact congr_arg PosNum.bit0 hm
[GOAL]
⊢ ∀ (n : Num), decodeNum (encodeNum n) = n
[PROOFSTEP]
intro n
[GOAL]
n : Num
⊢ decodeNum (encodeNum n) = n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero
[PROOFSTEP]
unfold encodeNum decodeNum
[GOAL]
case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n
[PROOFSTEP]
unfold encodeNum decodeNum
[GOAL]
case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero
[PROOFSTEP]
rfl
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
[PROOFSTEP]
rw [decode_encodePosNum n]
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
[PROOFSTEP]
rw [PosNum.cast_to_num]
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
[PROOFSTEP]
exact if_neg (encodePosNum_nonempty n)
[GOAL]
⊢ ∀ (n : ℕ), decodeNat (encodeNat n) = n
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ decodeNat (encodeNat n) = n
[PROOFSTEP]
conv_rhs => rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n
[PROOFSTEP]
exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)
[GOAL]
x : ℕ
⊢ decodeNat (List.map sectionΓ'Bool ((fun x => List.map inclusionBoolΓ' (encodeNat x)) x)) = x
[PROOFSTEP]
rw [List.map_map, leftInverse_section_inclusion.id, List.map_id, decode_encodeNat]
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ #α ≤ ℵ₀
[PROOFSTEP]
refine' Cardinal.lift_le.1 (e.card_le_card_list.trans _)
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ lift #(List e.Γ) ≤ lift ℵ₀
[PROOFSTEP]
simp only [Cardinal.lift_aleph0, Cardinal.lift_le_aleph0]
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
cases' isEmpty_or_nonempty e.Γ with h h
[GOAL]
case inl
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : IsEmpty e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
simp only [Cardinal.mk_le_aleph0]
[GOAL]
case inr
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : Nonempty e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
rw [Cardinal.mk_list_eq_aleph0]
