[GOAL]
α : Type u_1
inst✝ : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l
[PROOFSTEP]
induction' l with a l IH
[GOAL]
case nil
α : Type u_1
inst✝ : Encodable α
⊢ decodeList (encodeList []) = some []
[PROOFSTEP]
simp [encodeList, decodeList, unpair_pair, encodek, *]
[GOAL]
case cons
α : Type u_1
inst✝ : Encodable α
a : α
l : List α
IH : decodeList (encodeList l) = some l
⊢ decodeList (encodeList (a :: l)) = some (a :: l)
[PROOFSTEP]
simp [encodeList, decodeList, unpair_pair, encodek, *]
[GOAL]
α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)
[PROOFSTEP]
haveI := Encodable.ofCountable α
[GOAL]
α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
this : Encodable α
⊢ Countable (List α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ decodeList 0 = some []
[PROOFSTEP]
rw [decodeList]
[GOAL]
α : Type u_1
inst✝ : Encodable α
v : ℕ
⊢ decodeList (succ v) = Seq.seq ((fun x x_1 => x :: x_1) <$> decode (unpair v).fst) fun x => decode (unpair v).snd
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList (succ v) = Seq.seq ((fun x x_1 => x :: x_1) <$> decode (v₁, v₂).fst) fun x => decode (v₁, v₂).snd
[PROOFSTEP]
simp [decodeList, e]
[GOAL]
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode v₁)) fun x => decodeList v₂) =
    Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode v₁)) fun x => decode v₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Encodable α
a b : α
⊢ Decidable (Encodable.enle a b)
[PROOFSTEP]
unfold enle Order.Preimage
[GOAL]
α : Type u_1
inst✝ : Encodable α
a b : α
⊢ Decidable ((fun x x_1 => x ≤ x_1) (encode a) (encode b))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : Encodable α
s : Multiset α
⊢ decodeMultiset (encodeMultiset s) = some s
[PROOFSTEP]
simp [encodeMultiset, decodeMultiset, encodek]
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α
[PROOFSTEP]
classical exact (Fintype.truncEncodable α).out
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α
[PROOFSTEP]
exact (Fintype.truncEncodable α).out
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decodeList 0 ∧ encodeList a = 0
[PROOFSTEP]
rw [decodeList]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ some [] ∧ encodeList a = 0
[PROOFSTEP]
exact ⟨_, rfl, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v : ℕ
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
have h := unpair_right_le v
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).snd ≤ v
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rw [e] at h 
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rcases have : v₂ < succ v := lt_succ_of_le h
  denumerable_list_aux v₂ with
  ⟨a, h₁, h₂⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rw [Option.mem_def] at h₁ 
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
use ofNat α v₁ :: a
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList (succ v) ∧ encodeList (ofNat α v₁ :: a) = succ v
[PROOFSTEP]
simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ofNat (List α) 0 = []
[PROOFSTEP]
rw [← @encode_list_nil α, ofNat_encode]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v : ℕ
⊢ decodeList (succ v) = some (ofNat α (unpair v).fst :: ofNat (List α) (unpair v).snd)
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList (succ v) = some (ofNat α (v₁, v₂).fst :: ofNat (List α) (v₁, v₂).snd)
[PROOFSTEP]
simp [decodeList, e]
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (Seq.seq (some fun x => ofNat α v₁ :: x) fun x => decodeList v₂) = some (ofNat α v₁ :: ofNat (List α) v₂)
[PROOFSTEP]
rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some, Option.some.injEq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l
[PROOFSTEP]
rw [raise, lower, add_tsub_cancel_right, lower_raise l]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
⊢ raise (lower (m :: l) n) n = m :: l
[PROOFSTEP]
have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise, lower, tsub_add_cancel_of_le this, raise_lower h.of_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Multiset α
⊢ (fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0)) s) =
    s
[PROOFSTEP]
have := raise_lower (List.sorted_cons.2 ⟨fun n _ => Nat.zero_le n, (s.map encode).sort_sorted _⟩)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Multiset α
this :
  raise (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0) 0 =
    Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)
⊢ (fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0)) s) =
    s
[PROOFSTEP]
simp [-Multiset.coe_map, this]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0))
      ((fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0)) n) =
    n
[PROOFSTEP]
simp [-Multiset.coe_map, List.mergeSort_eq_self _ (raise_sorted _ _), lower_raise]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
⊢ lower' (raise' (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise', lower', add_tsub_cancel_right, lower_raise']
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
⊢ raise' (lower' (m :: l) n) n = m :: l
[PROOFSTEP]
have : n ≤ m := h₁ _ (l.mem_cons_self _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise', lower', tsub_add_cancel_of_le this, raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Finset α
⊢ ((fun n => Finset.map (Equiv.toEmbedding (eqv α).symm) (raise'Finset (ofNat (List ℕ) n) 0))
        ((fun s => encode (lower' (Finset.sort (fun x x_1 => x ≤ x_1) (Finset.map (Equiv.toEmbedding (eqv α)) s)) 0))
          s)).val =
    s.val
[PROOFSTEP]
simp [-Multiset.coe_map, raise'Finset, raise_lower' (fun n _ => Nat.zero_le n) (Finset.sort_sorted_lt _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (fun s => encode (lower' (Finset.sort (fun x x_1 => x ≤ x_1) (Finset.map (Equiv.toEmbedding (eqv α)) s)) 0))
      ((fun n => Finset.map (Equiv.toEmbedding (eqv α).symm) (raise'Finset (ofNat (List ℕ) n) 0)) n) =
    n
[PROOFSTEP]
simp [-Multiset.coe_map, Finset.map, raise'Finset, Finset.sort,
  List.mergeSort_eq_self (· ≤ ·) ((raise'_sorted _ _).imp (@le_of_lt _ _)), lower_raise']
[GOAL]
u : List Unit
⊢ length ((fun n => replicate n ()) (length u)) = length u
[PROOFSTEP]
simp
