-- Mathlib/Logic/Equiv/List.lean
theorem denumerable_list_aux : ∀ n : ℕ, ∃ a ∈ @decodeList α _ n, encodeList a = n
  | 0 => by rw [decodeList]; exact ⟨_, rfl, rfl⟩
  | succ v => by
    rcases e : unpair v with ⟨v₁, v₂⟩
    have h := unpair_right_le v
    rw [e] at h
    rcases have : v₂ < succ v := lt_succ_of_le h
      denumerable_list_aux v₂ with
      ⟨a, h₁, h₂⟩
    rw [Option.mem_def] at h₁
    use ofNat α v₁ :: a
    simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]

Proof state:
case mk.intro.intro
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rw [Option.mem_def] at h₁

Result:
case mk.intro.intro
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Proof state:
α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ some [], encodeList a = 0

Tactic:
exact ⟨_, rfl, rfl⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rw [e] at h

Result:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Proof state:
case mk.intro.intro
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
use ofNat α v₁ :: a

Result:
case h
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList v.succ ∧ encodeList (ofNat α v₁ :: a) = v.succ

Proof state:
α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ decodeList 0, encodeList a = 0

Tactic:
rw [decodeList]

Result:
α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ some [], encodeList a = 0

Proof state:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rcases have : v₂ < succ v := lt_succ_of_le h
  denumerable_list_aux v₂ with
  ⟨a, h₁, h₂⟩

Result:
case mk.intro.intro
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Proof state:
α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Result:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Proof state:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
have h := unpair_right_le v

Result:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Proof state:
case h
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList v.succ ∧ encodeList (ofNat α v₁ :: a) = v.succ

Tactic:
simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]

Result:
no goals