α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ some [] ∧ encodeList a = 0
α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decodeList 0 ∧ encodeList a = 0
rw [decodeList]
no goals
α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ some [] ∧ encodeList a = 0
exact ⟨_, rfl, rfl⟩
case mk
α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v : ℕ
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
cases' e : unpair v with v₁ v₂
case mk
α : Type u_1
β : Type ?u.30505
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
case mk
α : Type u_1
β : Type ?u.30505
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
have h := unpair_right_le v
case mk
α : Type u_1
β : Type ?u.30505
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
case mk
α : Type u_1
β : Type ?u.30505
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
rw [e] at h
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
case mk
α : Type u_1
β : Type ?u.30505
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
rcases have : v₂ < succ v := lt_succ_of_le h
  denumerable_list_aux v₂ with
  ⟨a, h₁, h₂⟩
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
rw [Option.mem_def] at h₁
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
use ofNat α v₁ :: a
no goals
case mk.intro.intro
α : Type u_1
β : Type ?u.30505
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
simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]