[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
⊢ ∀ (a : ℕ), Acc (Nat.lbp p) a
[PROOFSTEP]
let ⟨n, pn⟩ := H
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
⊢ ∀ (a : ℕ), Acc (Nat.lbp p) a
[PROOFSTEP]
suffices ∀ m k, n ≤ k + m → Acc (lbp p) k by exact fun a => this _ _ (Nat.le_add_left _ _)
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
this : ∀ (m k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
⊢ ∀ (a : ℕ), Acc (Nat.lbp p) a
[PROOFSTEP]
exact fun a => this _ _ (Nat.le_add_left _ _)
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
⊢ ∀ (m k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
[PROOFSTEP]
intro m k kn
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m k : ℕ
kn : n ≤ k + m
⊢ Acc (Nat.lbp p) k
[PROOFSTEP]
induction' m with m IH generalizing k
[GOAL]
case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m k✝ : ℕ
kn✝ : n ≤ k✝ + m
k : ℕ
kn : n ≤ k + zero
⊢ Acc (Nat.lbp p) k
[PROOFSTEP]
refine' ⟨_, fun y r => _⟩
[GOAL]
case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m✝ k✝ : ℕ
kn✝ : n ≤ k✝ + m✝
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
k : ℕ
kn : n ≤ k + succ m
⊢ Acc (Nat.lbp p) k
[PROOFSTEP]
refine' ⟨_, fun y r => _⟩
[GOAL]
case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m k✝ : ℕ
kn✝ : n ≤ k✝ + m
k : ℕ
kn : n ≤ k + zero
y : ℕ
r : Nat.lbp p y k
⊢ Acc (Nat.lbp p) y
[PROOFSTEP]
rcases r with ⟨rfl, a⟩
[GOAL]
case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m✝ k✝ : ℕ
kn✝ : n ≤ k✝ + m✝
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
k : ℕ
kn : n ≤ k + succ m
y : ℕ
r : Nat.lbp p y k
⊢ Acc (Nat.lbp p) y
[PROOFSTEP]
rcases r with ⟨rfl, a⟩
[GOAL]
case zero.intro
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m k✝ : ℕ
kn✝ : n ≤ k✝ + m
k : ℕ
kn : n ≤ k + zero
a : ∀ (k_1 : ℕ), k_1 ≤ k → false ∈ p k_1
⊢ Acc (Nat.lbp p) (k + 1)
[PROOFSTEP]
injection mem_unique pn.1 (a _ kn)
[GOAL]
case succ.intro
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m✝ k✝ : ℕ
kn✝ : n ≤ k✝ + m✝
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
k : ℕ
kn : n ≤ k + succ m
a : ∀ (k_1 : ℕ), k_1 ≤ k → false ∈ p k_1
⊢ Acc (Nat.lbp p) (k + 1)
[PROOFSTEP]
exact IH _ (by rw [Nat.add_right_comm]; exact kn)
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m✝ k✝ : ℕ
kn✝ : n ≤ k✝ + m✝
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
k : ℕ
kn : n ≤ k + succ m
a : ∀ (k_1 : ℕ), k_1 ≤ k → false ∈ p k_1
⊢ n ≤ k + 1 + m
[PROOFSTEP]
rw [Nat.add_right_comm]
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m✝ k✝ : ℕ
kn✝ : n ≤ k✝ + m✝
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (Nat.lbp p) k
k : ℕ
kn : n ≤ k + succ m
a : ∀ (k_1 : ℕ), k_1 ≤ k → false ∈ p k_1
⊢ n ≤ k + m + 1
[PROOFSTEP]
exact kn
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
⊢ (x : ℕ) →
    ((y : ℕ) →
        Nat.lbp p y x → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }) →
      (∀ (n : ℕ), n < x → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
[PROOFSTEP]
intro m IH al
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
⊢ { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
[PROOFSTEP]
have pm : (p m).Dom := by
  rcases H with ⟨n, h₁, h₂⟩
  rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
  · exact h₂ _ h₃
  · rw [h₃]
    exact h₁.fst
  · injection mem_unique h₁ (al _ h₃)
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
⊢ (p m).Dom
[PROOFSTEP]
rcases H with ⟨n, h₁, h₂⟩
[GOAL]
case intro.intro
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ (k : ℕ), k < n → (p k).Dom
⊢ (p m).Dom
[PROOFSTEP]
rcases lt_trichotomy m n with (h₃ | h₃ | h₃)
[GOAL]
case intro.intro.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ (k : ℕ), k < n → (p k).Dom
h₃ : m < n
⊢ (p m).Dom
[PROOFSTEP]
exact h₂ _ h₃
[GOAL]
case intro.intro.inr.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ (k : ℕ), k < n → (p k).Dom
h₃ : m = n
⊢ (p m).Dom
[PROOFSTEP]
rw [h₃]
[GOAL]
case intro.intro.inr.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ (k : ℕ), k < n → (p k).Dom
h₃ : m = n
⊢ (p n).Dom
[PROOFSTEP]
exact h₁.fst
[GOAL]
case intro.intro.inr.inr
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ (k : ℕ), k < n → (p k).Dom
h₃ : n < m
⊢ (p m).Dom
[PROOFSTEP]
injection mem_unique h₁ (al _ h₃)
[GOAL]
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
⊢ { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
[PROOFSTEP]
cases e : (p m).get pm
[GOAL]
case false
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
⊢ { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
[PROOFSTEP]
suffices ∀ᵉ k ≤ m, false ∈ p k from IH _ ⟨rfl, this⟩ fun n h => this _ (le_of_lt_succ h)
[GOAL]
case false
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
⊢ ∀ (k : ℕ), k ≤ m → false ∈ p k
[PROOFSTEP]
intro n h
[GOAL]
case false
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
n : ℕ
h : n ≤ m
⊢ false ∈ p n
[PROOFSTEP]
cases' h.lt_or_eq_dec with h h
[GOAL]
case false.inl
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
n : ℕ
h✝ : n ≤ m
h : n < m
⊢ false ∈ p n
[PROOFSTEP]
exact al _ h
[GOAL]
case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p n
[PROOFSTEP]
rw [h]
[GOAL]
case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p m
[PROOFSTEP]
exact ⟨_, e⟩
[GOAL]
case true
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ (k : ℕ), k < n → (p k).Dom
m : ℕ
IH : (y : ℕ) → Nat.lbp p y m → (∀ (n : ℕ), n < y → false ∈ p n) → { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
al : ∀ (n : ℕ), n < m → false ∈ p n
pm : (p m).Dom
e : Part.get (p m) pm = true
⊢ { n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }
[PROOFSTEP]
exact ⟨m, ⟨_, e⟩, al⟩
[GOAL]
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p
[PROOFSTEP]
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
[GOAL]
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
⊢ n ∈ rfind p
[PROOFSTEP]
rcases lt_trichotomy m n with (h | h | h)
[GOAL]
case inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p
[PROOFSTEP]
injection mem_unique (h₂ h) (rfind_spec hm)
[GOAL]
case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p
[PROOFSTEP]
rwa [← h]
[GOAL]
case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p
[PROOFSTEP]
injection mem_unique h₁ (rfind_min hm h)
[GOAL]
p : ℕ → Bool
m : ℕ
pm : p m = true
this : true ∈ ↑p m
n : ℕ
hn : n ∈ rfind ↑p
h : m < n
⊢ False
[PROOFSTEP]
injection mem_unique this (rfind_min hn h)
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
⊢ (rfindOpt f).Dom
[PROOFSTEP]
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
⊢ (rfindOpt f).Dom
[PROOFSTEP]
have s := Nat.find_spec h'
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
⊢ (rfindOpt f).Dom
[PROOFSTEP]
have fd : (rfind fun n => (f n).isSome).Dom := ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
⊢ true ∈ (fun n => ↑(Option.some (Option.isSome (f n)))) (Nat.find h')
[PROOFSTEP]
simpa using s.symm
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ (rfindOpt f).Dom
[PROOFSTEP]
refine' ⟨fd, _⟩
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
[PROOFSTEP]
have := rfind_spec (get_mem fd)
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this : true ∈ ↑(Option.some (Option.isSome (f (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) fd))))
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
[PROOFSTEP]
simp at this ⊢
[GOAL]
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
[PROOFSTEP]
cases' Option.isSome_iff_exists.1 this.symm with a e
[GOAL]
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
[PROOFSTEP]
rw [e]
[GOAL]
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome (Option.some a) = true
[PROOFSTEP]
trivial
[GOAL]
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
⊢ a ∈ rfindOpt f
[PROOFSTEP]
have h' := rfindOpt_dom.2 ⟨_, _, h⟩
[GOAL]
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
⊢ a ∈ rfindOpt f
[PROOFSTEP]
cases' rfindOpt_spec ⟨h', rfl⟩ with k hk
[GOAL]
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : Part.get (rfindOpt f) h' ∈ f k
⊢ a ∈ rfindOpt f
[PROOFSTEP]
have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
[GOAL]
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : Part.get (rfindOpt f) h' ∈ f k
this : Option.some a = Option.some (Part.get (rfindOpt f) h')
⊢ a ∈ rfindOpt f
[PROOFSTEP]
simp at this 
[GOAL]
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : Part.get (rfindOpt f) h' ∈ f k
this : a = Part.get (rfindOpt f) h'
⊢ a ∈ rfindOpt f
[PROOFSTEP]
simp [this, get_mem]
[GOAL]
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Partrec ↑f
[PROOFSTEP]
induction hf with
| zero => exact zero
| succ => exact succ
| left => exact left
| right => exact right
| pair _ _ pf pg =>
  refine' (pf.pair pg).of_eq_tot fun n => _
  simp [Seq.seq]
| comp _ _ pf pg =>
  refine' (pf.comp pg).of_eq_tot fun n => _
  simp
| prec _ _ pf pg =>
  refine' (pf.prec pg).of_eq_tot fun n => _
  simp only [unpaired, PFun.coe_val, bind_eq_bind]
  induction n.unpair.2 with
  | zero => simp
  | succ m IH =>
    simp only [mem_bind_iff, mem_some_iff]
    exact ⟨_, IH, rfl⟩
[GOAL]
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Partrec ↑f
[PROOFSTEP]
induction hf with
| zero => exact zero
| succ => exact succ
| left => exact left
| right => exact right
| pair _ _ pf pg =>
  refine' (pf.pair pg).of_eq_tot fun n => _
  simp [Seq.seq]
| comp _ _ pf pg =>
  refine' (pf.comp pg).of_eq_tot fun n => _
  simp
| prec _ _ pf pg =>
  refine' (pf.prec pg).of_eq_tot fun n => _
  simp only [unpaired, PFun.coe_val, bind_eq_bind]
  induction n.unpair.2 with
  | zero => simp
  | succ m IH =>
    simp only [mem_bind_iff, mem_some_iff]
    exact ⟨_, IH, rfl⟩
[GOAL]
case zero
f : ℕ → ℕ
⊢ Partrec ↑fun x => 0
[PROOFSTEP]

| zero => exact zero
[GOAL]
case zero
f : ℕ → ℕ
⊢ Partrec ↑fun x => 0
[PROOFSTEP]
exact zero
[GOAL]
case succ
f : ℕ → ℕ
⊢ Partrec ↑Nat.succ
[PROOFSTEP]

| succ => exact succ
[GOAL]
case succ
f : ℕ → ℕ
⊢ Partrec ↑Nat.succ
[PROOFSTEP]
exact succ
[GOAL]
case left
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).fst
[PROOFSTEP]

| left => exact left
[GOAL]
case left
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).fst
[PROOFSTEP]
exact left
[GOAL]
case right
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).snd
[PROOFSTEP]

| right => exact right
[GOAL]
case right
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).snd
[PROOFSTEP]
exact right
[GOAL]
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => Nat.pair (f✝ n) (g✝ n)
[PROOFSTEP]

| pair _ _ pf pg =>
  refine' (pf.pair pg).of_eq_tot fun n => _
  simp [Seq.seq]
[GOAL]
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => Nat.pair (f✝ n) (g✝ n)
[PROOFSTEP]
refine' (pf.pair pg).of_eq_tot fun n => _
[GOAL]
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.pair (f✝ n) (g✝ n) ∈ Seq.seq (Nat.pair <$> ↑f✝ n) fun x => ↑g✝ n
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => f✝ (g✝ n)
[PROOFSTEP]

| comp _ _ pf pg =>
  refine' (pf.comp pg).of_eq_tot fun n => _
  simp
[GOAL]
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => f✝ (g✝ n)
[PROOFSTEP]
refine' (pf.comp pg).of_eq_tot fun n => _
[GOAL]
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝
[PROOFSTEP]
simp
[GOAL]
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑(unpaired fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n)
[PROOFSTEP]

| prec _ _ pf pg =>
  refine' (pf.prec pg).of_eq_tot fun n => _
  simp only [unpaired, PFun.coe_val, bind_eq_bind]
  induction n.unpair.2 with
  | zero => simp
  | succ m IH =>
    simp only [mem_bind_iff, mem_some_iff]
    exact ⟨_, IH, rfl⟩
[GOAL]
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑(unpaired fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n)
[PROOFSTEP]
refine' (pf.prec pg).of_eq_tot fun n => _
[GOAL]
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n) n ∈
    unpaired
      (fun a n =>
        Nat.rec (↑f✝ a)
          (fun y IH => do
            let i ← IH
            ↑g✝ (Nat.pair a (Nat.pair y i)))
          n)
      n
[PROOFSTEP]
simp only [unpaired, PFun.coe_val, bind_eq_bind]
[GOAL]
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (unpair n).snd ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (unpair n).snd
[PROOFSTEP]
induction n.unpair.2 with
| zero => simp
| succ m IH =>
  simp only [mem_bind_iff, mem_some_iff]
  exact ⟨_, IH, rfl⟩
[GOAL]
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n x✝ : ℕ
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) x✝ ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) x✝
[PROOFSTEP]
induction n.unpair.2 with
| zero => simp
| succ m IH =>
  simp only [mem_bind_iff, mem_some_iff]
  exact ⟨_, IH, rfl⟩
[GOAL]
case prec.zero
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) Nat.zero ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case prec.zero
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) Nat.zero ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (Nat.succ m) ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (Nat.succ m)
[PROOFSTEP]

| succ m IH =>
  simp only [mem_bind_iff, mem_some_iff]
  exact ⟨_, IH, rfl⟩
[GOAL]
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (Nat.succ m) ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (Nat.succ m)
[PROOFSTEP]
simp only [mem_bind_iff, mem_some_iff]
[GOAL]
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ ∃ a,
    a ∈
        Nat.rec (Part.some (f✝ (unpair n).fst))
          (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m ∧
      g✝
          (Nat.pair (unpair n).fst
            (Nat.pair m (Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m))) =
        g✝ (Nat.pair (unpair n).fst (Nat.pair m a))
[PROOFSTEP]
exact ⟨_, IH, rfl⟩
[GOAL]
n a : ℕ
x✝ : a ∈ Nat.rfind fun n_1 => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair n n_1)
h : (Nat.rfind fun n_1 => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair n n_1)).Dom
h✝ : Part.get (Nat.rfind fun n_1 => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair n n_1)) h = a
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
f g h : ℕ →. ℕ
hf : Partrec f
hg : Partrec g
hh : Partrec h
a s : ℕ
⊢ (s ∈
      (Seq.seq (Nat.pair <$> Part.some a) fun x => f a) >>=
        unpaired fun a n =>
          Nat.rec (g a)
            (fun y IH => do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n) ↔
    s ∈
      Part.bind (f a) fun n =>
        Nat.rec (g a)
          (fun y IH => do
            let i ← IH
            h (Nat.pair a (Nat.pair y i)))
          n
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$> ↑(unpaired fun n m => if n = Nat.succ m then 0 else 1) (Nat.pair n n_1)) =
    ↑(Nat.ppred n)
[PROOFSTEP]
cases n
[GOAL]
case zero
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
⊢ (Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$> ↑(unpaired fun n m => if n = Nat.succ m then 0 else 1) (Nat.pair Nat.zero n)) =
    ↑(Nat.ppred Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$> ↑(unpaired fun n m => if n = Nat.succ m then 0 else 1) (Nat.pair (Nat.succ n✝) n)) =
    ↑(Nat.ppred (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
case zero
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
⊢ (Nat.rfind fun n => Part.some false) = Part.none
[PROOFSTEP]
exact eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by simp [show 0 ≠ m.succ by intro h; injection h] at h 
[GOAL]
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h : true ∈ (fun n => Part.some false) m
right✝ : ∀ (k : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
⊢ False
[PROOFSTEP]
simp [show 0 ≠ m.succ by intro h; injection h] at h 
[GOAL]
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h : true ∈ (fun n => Part.some false) m
right✝ : ∀ (k : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
⊢ 0 ≠ Nat.succ m
[PROOFSTEP]
intro h
[GOAL]
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h✝¹ : true ∈ (fun n => Part.some false) m
right✝ : ∀ (k : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
h : 0 = Nat.succ m
⊢ False
[PROOFSTEP]
injection h
[GOAL]
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))) = Part.some n✝
[PROOFSTEP]
refine' eq_some_iff.2 _
[GOAL]
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ n✝ ∈ Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))
[PROOFSTEP]
simp
[GOAL]
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬(¬n✝ = m → False)
[PROOFSTEP]
intro m h
[GOAL]
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ m : ℕ
h : m < n✝
⊢ ¬(¬n✝ = m → False)
[PROOFSTEP]
simp [ne_of_gt h]
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (do
      let n ← (↑fun n => encode (Option.map f (decode n))) n
      ↑(Nat.ppred n)) =
    Part.bind ↑(decode n) fun a => map encode (↑f a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(Nat.ppred (encode (Option.map f (decode n)))) = Part.bind ↑(decode n) fun a => Part.some (encode (f a))
[PROOFSTEP]
cases decode (α := α) n
[GOAL]
case none
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(Nat.ppred (encode (Option.map f Option.none))) = Part.bind ↑Option.none fun a => Part.some (encode (f a))
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
val✝ : α
⊢ ↑(Nat.ppred (encode (Option.map f (Option.some val✝)))) =
    Part.bind ↑(Option.some val✝) fun a => Part.some (encode (f a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← Part.bind ↑(decode n) fun a => map encode (↑f a)
      ↑(Nat.ppred n)) =
    Part.bind ↑(decode n) fun a => map encode ((fun a => ↑(f a)) a)
[PROOFSTEP]
cases' decode (α := α) n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← Part.bind ↑Option.none fun a => map encode (↑f a)
      ↑(Nat.ppred n)) =
    Part.bind ↑Option.none fun a => map encode ((fun a => ↑(f a)) a)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (do
      let n ← Part.bind ↑(Option.some a) fun a => map encode (↑f a)
      ↑(Nat.ppred n)) =
    Part.bind ↑(Option.some a) fun a => map encode ((fun a => ↑(f a)) a)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(Nat.ppred (encode (f a))) = map encode ↑(f a)
[PROOFSTEP]
cases' f a with b
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(Nat.ppred (encode Option.none)) = map encode ↑Option.none
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
b : β
⊢ ↑(Nat.ppred (encode (Option.some b))) = map encode ↑(Option.some b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ (Seq.seq (Nat.pair <$> Part.bind ↑(decode n) fun a => map encode (↑f a)) fun x =>
      Part.bind ↑(decode n) fun a => map encode (↑g a)) =
    Part.bind ↑(decode n) fun a => map encode ((↑fun a => (f a, g a)) a)
[PROOFSTEP]
cases decode (α := α) n
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ (Seq.seq (Nat.pair <$> Part.bind ↑Option.none fun a => map encode (↑f a)) fun x =>
      Part.bind ↑Option.none fun a => map encode (↑g a)) =
    Part.bind ↑Option.none fun a => map encode ((↑fun a => (f a, g a)) a)
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
val✝ : α
⊢ (Seq.seq (Nat.pair <$> Part.bind ↑(Option.some val✝) fun a => map encode (↑f a)) fun x =>
      Part.bind ↑(Option.some val✝) fun a => map encode (↑g a)) =
    Part.bind ↑(Option.some val✝) fun a => map encode ((↑fun a => (f a, g a)) a)
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = Part.bind ↑(decode n) fun a => map encode ((fun x => Part.none) a)
[PROOFSTEP]
cases decode (α := α) n
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = Part.bind ↑Option.none fun a => map encode ((fun x => Part.none) a)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ Part.none = Part.bind ↑(Option.some val✝) fun a => map encode ((fun x => Part.none) a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (do
      let n ← Seq.seq (Nat.pair <$> Part.some n) fun x => Part.bind ↑(decode n) fun a => map encode (f a)
      Part.bind ↑(decode n) fun a => map encode ((fun p => g p.fst p.snd) a)) =
    Part.bind ↑(decode n) fun a => map encode ((fun a => Part.bind (f a) (g a)) a)
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (Part.bind (Part.bind ↑(decode n) fun y => map (Nat.pair n) (map encode (f y))) fun n =>
      Part.bind ↑(Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
        fun a => map encode (g a.fst a.snd)) =
    Part.bind ↑(decode n) fun a => Part.bind (f a) fun y => map encode (g a y)
[PROOFSTEP]
cases' e : decode (α := α) n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
e : decode n = Option.none
⊢ (Part.bind (Part.bind ↑Option.none fun y => map (Nat.pair n) (map encode (f y))) fun n =>
      Part.bind ↑(Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
        fun a => map encode (g a.fst a.snd)) =
    Part.bind ↑Option.none fun a => Part.bind (f a) fun y => map encode (g a y)
[PROOFSTEP]
simp [e, encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Part.bind (Part.bind ↑(Option.some a) fun y => map (Nat.pair n) (map encode (f y))) fun n =>
      Part.bind ↑(Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
        fun a => map encode (g a.fst a.snd)) =
    Part.bind ↑(Option.some a) fun a => Part.bind (f a) fun y => map encode (g a y)
[PROOFSTEP]
simp [e, encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β → σ
hf : Partrec f
hg : Computable₂ g
⊢ Partrec fun a => Part.map (g a) (f a)
[PROOFSTEP]
simpa [bind_some_eq_map] using @Partrec.bind _ _ _ _ _ _ _ (fun a => Part.some ∘ (g a)) hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ (Part.bind (Part.bind ↑(decode n) fun a => Part.map encode (↑f a)) fun n_1 =>
      Nat.rec (Part.bind ↑(decode n) fun a => Part.map encode (g a))
        (fun y IH => do
          let i ← IH
          Part.bind ↑(decode (Nat.pair n (Nat.pair y i))) fun a => Part.map encode ((fun p => h p.fst p.snd) a))
        n_1) =
    Part.bind ↑(decode n) fun a =>
      Part.map encode ((fun a => Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) (f a)) a)
[PROOFSTEP]
cases' e : decode (α := α) n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
e : decode n = Option.none
⊢ (Part.bind (Part.bind ↑Option.none fun a => Part.map encode (↑f a)) fun n_1 =>
      Nat.rec (Part.bind ↑Option.none fun a => Part.map encode (g a))
        (fun y IH => do
          let i ← IH
          Part.bind ↑(decode (Nat.pair n (Nat.pair y i))) fun a => Part.map encode ((fun p => h p.fst p.snd) a))
        n_1) =
    Part.bind ↑Option.none fun a =>
      Part.map encode ((fun a => Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) (f a)) a)
[PROOFSTEP]
simp [e]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Part.bind (Part.bind ↑(Option.some a) fun a => Part.map encode (↑f a)) fun n_1 =>
      Nat.rec (Part.bind ↑(Option.some a) fun a => Part.map encode (g a))
        (fun y IH => do
          let i ← IH
          Part.bind ↑(decode (Nat.pair n (Nat.pair y i))) fun a => Part.map encode ((fun p => h p.fst p.snd) a))
        n_1) =
    Part.bind ↑(Option.some a) fun a =>
      Part.map encode ((fun a => Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) (f a)) a)
[PROOFSTEP]
simp [e]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      (f a) =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) (f a))
[PROOFSTEP]
induction' f a with m IH
[GOAL]
case some.zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      Nat.zero =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case some.succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m)
⊢ Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      (Nat.succ m) =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) (Nat.succ m))
[PROOFSTEP]
simp
[GOAL]
case some.succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m)
⊢ (Part.bind
      (Nat.rec (Part.map encode (g a))
        (fun y IH =>
          Part.bind IH fun i =>
            Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
        m)
      fun i => Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode i)) fun a => Part.map encode (h a.fst a.snd)) =
    Part.bind (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m) fun y => Part.map encode (h a (m, y))
[PROOFSTEP]
rw [IH, Part.bind_map]
[GOAL]
case some.succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m)
⊢ (Part.bind (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m) fun y =>
      Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y))) fun a => Part.map encode (h a.fst a.snd)) =
    Part.bind (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m) fun y => Part.map encode (h a (m, y))
[PROOFSTEP]
congr
[GOAL]
case some.succ.e_g
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m)
⊢ (fun y =>
      Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y))) fun a => Part.map encode (h a.fst a.snd)) =
    fun y => Part.map encode (h a (m, y))
[PROOFSTEP]
funext s
[GOAL]
case some.succ.e_g.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        Part.bind IH fun i =>
          Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i)) fun a => Part.map encode (h a.fst a.snd))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => Part.bind IH fun i => h a (y, i)) m)
s : σ
⊢ (Part.bind ↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode s))) fun a => Part.map encode (h a.fst a.snd)) =
    Part.map encode (h a (m, s))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (do
      let n ← Part.bind ↑(decode n) fun a => Part.map encode (↑g a)
      Part.bind ↑(decode n) fun a => Part.map encode (f a)) =
    Part.bind ↑(decode n) fun a => Part.map encode ((fun a => f (g a)) a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (Part.bind (Part.bind ↑(decode n) fun a => Part.some (encode (g a))) fun n =>
      Part.bind ↑(decode n) fun a => Part.map encode (f a)) =
    Part.bind ↑(decode n) fun a => Part.map encode (f (g a))
[PROOFSTEP]
cases' e : decode (α := α) n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
e : decode n = Option.none
⊢ (Part.bind (Part.bind ↑Option.none fun a => Part.some (encode (g a))) fun n =>
      Part.bind ↑(decode n) fun a => Part.map encode (f a)) =
    Part.bind ↑Option.none fun a => Part.map encode (f (g a))
[PROOFSTEP]
simp [e, encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Part.bind (Part.bind ↑(Option.some a) fun a => Part.some (encode (g a))) fun n =>
      Part.bind ↑(decode n) fun a => Part.map encode (f a)) =
    Part.bind ↑(Option.some a) fun a => Part.map encode (f (g a))
[PROOFSTEP]
simp [e, encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f
[PROOFSTEP]
simp [Partrec, map_id']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f
[PROOFSTEP]
simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$>
        Part.bind ↑(decode (Nat.pair n n_1)) fun a =>
          Part.map encode ((fun a => Part.map (fun b => bif (a, b).snd then 0 else 1) (p a.fst a.snd)) a)) =
    Part.bind ↑(decode n) fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)
[PROOFSTEP]
cases' e : decode (α := α) n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
e : decode n = Option.none
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$>
        Part.bind ↑(decode (Nat.pair n n_1)) fun a =>
          Part.map encode ((fun a => Part.map (fun b => bif (a, b).snd then 0 else 1) (p a.fst a.snd)) a)) =
    Part.bind ↑Option.none fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)
[PROOFSTEP]
simp [e, Nat.rfind_zero_none, map_id']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$>
        Part.bind ↑(decode (Nat.pair n n_1)) fun a =>
          Part.map encode ((fun a => Part.map (fun b => bif (a, b).snd then 0 else 1) (p a.fst a.snd)) a)) =
    Part.bind ↑(Option.some a) fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)
[PROOFSTEP]
simp [e, Nat.rfind_zero_none, map_id']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) =
    Nat.rfind (p a)
[PROOFSTEP]
congr
[GOAL]
case some.e_p
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a
[PROOFSTEP]
funext n
[GOAL]
case some.e_p.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n)) = p a n
[PROOFSTEP]
simp [Part.map_map, (· ∘ ·)]
[GOAL]
case some.e_p.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun x => decide ((bif x then 0 else 1) = 0)) (p a n) = p a n
[PROOFSTEP]
refine map_id' (fun b => ?_) _
[GOAL]
case some.e_p.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
b : Bool
⊢ decide ((bif b then 0 else 1) = 0) = b
[PROOFSTEP]
cases b
[GOAL]
case some.e_p.h.false
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ decide ((bif false then 0 else 1) = 0) = false
[PROOFSTEP]
rfl
[GOAL]
case some.e_p.h.true
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ decide ((bif true then 0 else 1) = 0) = true
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH => Part.bind IH fun i => h (a, y, i).fst (Nat.pred (f (a, y, i).fst))) (f a) =
    Nat.casesOn (f a) (Part.some (g a)) (h a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a (Nat.pred (f a))) (f a) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)
[PROOFSTEP]
cases' f a with n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a (Nat.pred Nat.zero)) Nat.zero =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a (Nat.pred (Nat.succ n))) (Nat.succ n) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ (Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n) = h a n
[PROOFSTEP]
refine' ext fun b => ⟨fun H => _, fun H => _⟩
[GOAL]
case succ.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
⊢ b ∈ h a n
[PROOFSTEP]
rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
[GOAL]
case succ.refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
c : σ
left✝ : c ∈ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n
h₂ : b ∈ h a n
⊢ b ∈ h a n
[PROOFSTEP]
exact h₂
[GOAL]
case succ.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
[PROOFSTEP]
have : ∀ m, (Nat.rec (motive := fun _ => Part σ) (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom :=
  by
  intro m
  induction m <;> simp [*, H.fst]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
[PROOFSTEP]
intro m
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
[PROOFSTEP]
induction m
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) Nat.zero).Dom
[PROOFSTEP]
simp [*, H.fst]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
n✝ : ℕ
n_ih✝ : (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) n✝).Dom
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) (Nat.succ n✝)).Dom
[PROOFSTEP]
simp [*, H.fst]
[GOAL]
case succ.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
this : ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
[PROOFSTEP]
exact ⟨⟨this n, H.fst⟩, H.snd⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ
h : Nat.Partrec fun n => Part.bind ↑(decode₂ α n) fun a => Part.map encode (f a)
⊢ Partrec fun a => Part.map encode (f a)
[PROOFSTEP]
simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a => Vector.mOfFn fun i => f i a
[PROOFSTEP]
simp [Vector.mOfFn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a =>
    Part.bind (f 0 a) fun a_1 => Part.bind (Vector.mOfFn fun i => f (Fin.succ i) a) fun v => Part.some (a_1 ::ᵥ v)
[PROOFSTEP]
exact
  (hf 0).bind
    (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst) (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
⊢ (Part.bind ↑(decode n) fun a =>
      map encode
        ((fun a =>
            Part.bind
              (do
                let n ← (↑fun n => encode (decode n)) a.snd
                ↑(Nat.ppred n))
              ↑fun b => (fun a n => Option.bind (decode n) (f a)) (a, b).fst.fst (a, b).fst.snd)
          a)) =
    Part.bind ↑(decode n) fun a => map encode ((↑fun p => f p.fst p.snd) a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
⊢ (Part.bind ↑(Option.bind (decode (Nat.unpair n).fst) fun a => Option.some (a, (Nat.unpair n).snd)) fun a =>
      Part.bind ↑(Nat.ppred (encode (decode a.snd))) fun y =>
        Part.some (encode (Option.bind (decode a.snd) (f a.fst)))) =
    Part.bind ↑(Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
      fun a => Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
cases decode (α := α) n.unpair.1
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
⊢ (Part.bind ↑(Option.bind Option.none fun a => Option.some (a, (Nat.unpair n).snd)) fun a =>
      Part.bind ↑(Nat.ppred (encode (decode a.snd))) fun y =>
        Part.some (encode (Option.bind (decode a.snd) (f a.fst)))) =
    Part.bind ↑(Option.bind Option.none fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)) fun a =>
      Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
val✝ : α
⊢ (Part.bind ↑(Option.bind (Option.some val✝) fun a => Option.some (a, (Nat.unpair n).snd)) fun a =>
      Part.bind ↑(Nat.ppred (encode (decode a.snd))) fun y =>
        Part.some (encode (Option.bind (decode a.snd) (f a.fst)))) =
    Part.bind ↑(Option.bind (Option.some val✝) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)) fun a =>
      Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
val✝ : α
⊢ (Part.bind ↑(Nat.ppred (encode (decode (Nat.unpair n).snd))) fun y =>
      Part.some (encode (Option.bind (decode (Nat.unpair n).snd) (f val✝)))) =
    Part.bind ↑(Option.map (Prod.mk val✝) (decode (Nat.unpair n).snd)) fun a => Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
cases decode (α := β) n.unpair.2
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
val✝ : α
⊢ (Part.bind ↑(Nat.ppred (encode Option.none)) fun y => Part.some (encode (Option.bind Option.none (f val✝)))) =
    Part.bind ↑(Option.map (Prod.mk val✝) Option.none) fun a => Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => Option.bind (decode n) (f a)
n : ℕ
val✝¹ : α
val✝ : β
⊢ (Part.bind ↑(Nat.ppred (encode (Option.some val✝))) fun y =>
      Part.some (encode (Option.bind (Option.some val✝) (f val✝¹)))) =
    Part.bind ↑(Option.map (Prod.mk val✝¹) (Option.some val✝)) fun a => Part.some (encode (f a.fst a.snd))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂ fun a n => Option.bind (decode n) (f a)
[PROOFSTEP]
have :
  Partrec fun a : α × ℕ =>
    (encode (decode (α := β) a.2)).casesOn (some Option.none) fun n => Part.map (f a.1) (decode (α := β) n) :=
  Partrec.nat_casesOn_right (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
    (Primrec.encdec.to_comp.comp snd) (const Option.none)
    ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)
⊢ Computable₂ fun a n => Option.bind (decode n) (f a)
[PROOFSTEP]
refine' this.of_eq fun a => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)
a : α × ℕ
⊢ (Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)) =
    (↑fun p => (fun a n => Option.bind (decode n) (f a)) p.fst p.snd) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.fst) ↑(decode n)) (encode (decode a.snd)) =
    Part.some (Option.bind (decode a.snd) (f a.fst))
[PROOFSTEP]
cases decode (α := β) a.2
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.fst) ↑(decode n)) (encode Option.none) =
    Part.some (Option.bind Option.none (f a.fst))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.snd)) (Part.some Option.none) fun n => map (f a.fst) ↑(decode n)
a : α × ℕ
val✝ : β
⊢ Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.fst) ↑(decode n)) (encode (Option.some val✝)) =
    Part.some (Option.bind (Option.some val✝) (f a.fst))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Computable₂ fun a n => Option.map (f a) (decode n)) ↔ Computable₂ f
[PROOFSTEP]
convert (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff
[GOAL]
case h.e'_1.h.e'_7.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → σ
x✝¹ : α
x✝ : ℕ
⊢ Option.map (f x✝¹) (decode x✝) = Option.bind (decode x✝) (Option.some ∘ f x✝¹)
[PROOFSTEP]
apply Option.map_eq_bind
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH => Part.bind IH fun i => ↑(h a) (y, i)) (f a) =
    (↑fun a => Nat.rec (g a) (fun y IH => h a (y, IH)) (f a)) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => Part.some (h a (y, i))) (f a) =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) (f a))
[PROOFSTEP]
induction f a
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => Part.some (h a (y, i))) Nat.zero =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) Nat.zero)
[PROOFSTEP]
simp [*]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
n✝ : ℕ
n_ih✝ :
  Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => Part.some (h a (y, i))) n✝ =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) n✝)
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => Part.some (h a (y, i))) (Nat.succ n✝) =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) (Nat.succ n✝))
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b => f (a, b).fst) = bif c a then f a else g a
[PROOFSTEP]
cases c a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode false) (g a) fun b => f (a, b).fst) = bif false then f a else g a
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode true) (g a) fun b => f (a, b).fst) = bif true then f a else g a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n => Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))
[PROOFSTEP]
cases o a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode Option.none) (Option.some (f a)) fun n => Option.map (g a) (decode n)) =
    Option.some (Option.casesOn Option.none (f a) (g a))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ (Nat.casesOn (encode (Option.some val✝)) (Option.some (f a)) fun n => Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (Option.some val✝) (f a) (g a))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn (f a) Option.none (g a) = Option.bind (f a) (g a)
[PROOFSTEP]
cases f a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn Option.none Option.none (g a) = Option.bind Option.none (g a)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ Option.casesOn (Option.some val✝) Option.none (g a) = Option.bind (Option.some val✝) (g a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
⊢ Computable fun a => Option.map (g a) (f a)
[PROOFSTEP]
convert option_bind hf (option_some.comp₂ hg)
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
x✝ : α
⊢ Option.map (g x✝) (f x✝) = Option.bind (f x✝) fun b => Option.some (g x✝ b)
[PROOFSTEP]
apply Option.map_eq_bind
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn (f a) (g a) fun b => b) = Option.getD (f a) (g a)
[PROOFSTEP]
cases f a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn Option.none (g a) fun b => b) = Option.getD Option.none (g a)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val✝ : β
⊢ (Option.casesOn (Option.some val✝) (g a) fun b => b) = Option.getD (Option.some val✝) (g a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
⊢ (bif Nat.bodd (encode (f a)) then Option.map (h a) (decode (Nat.div2 (encode (f a))))
    else Option.map (g a) (decode (Nat.div2 (encode (f a))))) =
    Option.some (Sum.casesOn (f a) (g a) (h a))
[PROOFSTEP]
cases' f a with b c
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
b : β
⊢ (bif Nat.bodd (encode (Sum.inl b)) then Option.map (h a) (decode (Nat.div2 (encode (Sum.inl b))))
    else Option.map (g a) (decode (Nat.div2 (encode (Sum.inl b))))) =
    Option.some (Sum.casesOn (Sum.inl b) (g a) (h a))
[PROOFSTEP]
simp [Nat.div2_val]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
c : γ
⊢ (bif Nat.bodd (encode (Sum.inr c)) then Option.map (h a) (decode (Nat.div2 (encode (Sum.inr c))))
    else Option.map (g a) (decode (Nat.div2 (encode (Sum.inr c))))) =
    Option.some (Sum.casesOn (Sum.inr c) (g a) (h a))
[PROOFSTEP]
simp [Nat.div2_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        Option.bind (a, y, IH).snd.snd fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).fst.snd ++ [(((a, y, IH), b), b_1).snd])
            (g ((a, y, IH), b).fst.fst.fst ((a, y, IH), b).snd))
      a.snd =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.fst a.snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some []) (fun y IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a.fst b)) a.snd =
    Option.some (List.map (f a.fst) (List.range a.snd))
[PROOFSTEP]
induction' a.2 with n IH
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some []) (fun y IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a.fst b))
      Nat.zero =
    Option.some (List.map (f a.fst) (List.range Nat.zero))
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
n : ℕ
IH :
  Nat.rec (Option.some []) (fun y IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a.fst b)) n =
    Option.some (List.map (f a.fst) (List.range n))
⊢ Nat.rec (Option.some []) (fun y IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a.fst b))
      (Nat.succ n) =
    Option.some (List.map (f a.fst) (List.range (Nat.succ n)))
[PROOFSTEP]
simp [IH, H, List.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
this : Computable₂ fun a n => List.map (f a) (List.range n)
a : α × ℕ
⊢ (fun a b => List.get? (List.map (f (a, b).fst) (List.range (Nat.succ (a, b).snd))) (a, b).snd) a.fst a.snd =
    Option.some (f a.fst a.snd)
[PROOFSTEP]
simp [List.get?_range (Nat.lt_succ_self a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a => List.ofFn fun i => f i a
[PROOFSTEP]
simp [List.ofFn_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a => f 0 a :: List.ofFn fun i => f (Fin.succ i) a
[PROOFSTEP]
exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i => ↑(f i) a) = (↑fun a => Vector.ofFn fun i => f i a) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ
h : Partrec fun a => Part.map Option.some (f a)
n : ℕ
⊢ (do
      let n ← Part.bind ↑(decode n) fun a => Part.map encode ((fun a => Part.map Option.some (f a)) a)
      ↑(Nat.ppred n)) =
    Part.bind ↑(decode n) fun a => Part.map encode (f a)
[PROOFSTEP]
simp [Part.bind_assoc, ← Function.comp_apply (f := Part.some) (g := encode), bind_some_eq_map, -Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a => Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)
a : α
⊢ (Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)) =
    Option.casesOn (o a) (Part.some (f a)) (g a)
[PROOFSTEP]
cases' o a with b
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a => Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)
a : α
⊢ (Nat.casesOn (encode Option.none) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)) =
    Option.casesOn Option.none (Part.some (f a)) (g a)
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a => Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)
a : α
b : β
⊢ (Nat.casesOn (encode (Option.some b)) (Part.some (f a)) fun n => Part.bind (↑(decode n)) (g a)) =
    Option.casesOn (Option.some b) (Part.some (f a)) (g a)
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a =>
    Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a))
[PROOFSTEP]
cases f a
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a =>
    Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)
a : α
val✝ : β
⊢ (Option.casesOn (Sum.casesOn (Sum.inl val✝) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inl val✝) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (fun b => Part.some (g a b)) (h a))
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a =>
    Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)
a : α
val✝ : γ
⊢ (Option.casesOn (Sum.casesOn (Sum.inr val✝) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inr val✝) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (fun b => Part.some (g a b)) (h a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b => Sum.inr (a, b).snd) fun b => Sum.inl (a, b).snd) (fun b => Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c => Part.some (h a c)
[PROOFSTEP]
cases f a
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : β
⊢ Sum.casesOn (Sum.casesOn (Sum.inl val✝) (fun b => Sum.inr (a, b).snd) fun b => Sum.inl (a, b).snd)
      (fun b => Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inl val✝) (g a) fun c => Part.some (h a c)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : γ
⊢ Sum.casesOn (Sum.casesOn (Sum.inr val✝) (fun b => Sum.inr (a, b).snd) fun b => Sum.inl (a, b).snd)
      (fun b => Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inr val✝) (g a) fun c => Part.some (h a c)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
⊢ let F := fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n;
  (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ PFun.fix f a
[PROOFSTEP]
intro F
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
⊢ (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ PFun.fix f a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩
[GOAL]
case refine'_1.intro.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
have : ∀ (m a') (_ : Sum.inr a' ∈ F a m) (_ : b ∈ PFun.fix f a'), b ∈ PFun.fix f a :=
  by
  intro m a' am ba
  induction' m with m IH generalizing a' <;> simp at am 
  · rwa [← am]
  rcases am with ⟨a₂, am₂, fa₂⟩
  exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
⊢ ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
[PROOFSTEP]
intro m a' am ba
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ PFun.fix f a'
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
induction' m with m IH generalizing a'
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
a'✝ : α
am✝ : Sum.inr a'✝ ∈ F a m
ba✝ : b ∈ PFun.fix f a'✝
a' : α
am : Sum.inr a' ∈ F a Nat.zero
ba : b ∈ PFun.fix f a'
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
simp at am 
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m✝ : ℕ
a'✝ : α
am✝ : Sum.inr a'✝ ∈ F a m✝
ba✝ : b ∈ PFun.fix f a'✝
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
a' : α
am : Sum.inr a' ∈ F a (Nat.succ m)
ba : b ∈ PFun.fix f a'
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
simp at am 
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
a'✝ : α
am✝ : Sum.inr a'✝ ∈ F a m
ba✝ : b ∈ PFun.fix f a'✝
a' : α
ba : b ∈ PFun.fix f a'
am : a' = a
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
rwa [← am]
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m✝ : ℕ
a'✝ : α
am✝ : Sum.inr a'✝ ∈ F a m✝
ba✝ : b ∈ PFun.fix f a'✝
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
a' : α
ba : b ∈ PFun.fix f a'
am :
  ∃ b,
    Sum.inr b ∈
        Nat.rec (Part.some (Sum.inr a))
          (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) m ∧
      Sum.inr a' ∈ f b
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
rcases am with ⟨a₂, am₂, fa₂⟩
[GOAL]
case succ.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m✝ : ℕ
a'✝ : α
am : Sum.inr a'✝ ∈ F a m✝
ba✝ : b ∈ PFun.fix f a'✝
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
a' : α
ba : b ∈ PFun.fix f a'
a₂ : α
am₂ :
  Sum.inr a₂ ∈
    Nat.rec (Part.some (Sum.inr a))
      (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) m
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
[GOAL]
case refine'_1.intro.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
cases n
[GOAL]
case refine'_1.intro.intro.intro.zero
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
h₂ : Sum.inl b ∈ F a Nat.zero
_x : ∃ b', Sum.inl b' ∈ F a Nat.zero
h₁ : ∀ {m : ℕ}, m < Nat.zero → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
simp at h₂ 
[GOAL]
case refine'_1.intro.intro.intro.succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
n✝ : ℕ
h₂ : Sum.inl b ∈ F a (Nat.succ n✝)
_x : ∃ b', Sum.inl b' ∈ F a (Nat.succ n✝)
h₁ : ∀ {m : ℕ}, m < Nat.succ n✝ → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
simp at h₂ 
[GOAL]
case refine'_1.intro.intro.intro.succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (Nat.succ n✝)
h₁ : ∀ {m : ℕ}, m < Nat.succ n✝ → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a))
        (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
rcases h₂ with (h₂ | ⟨a', am', fa'⟩)
[GOAL]
case refine'_1.intro.intro.intro.succ.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (Nat.succ n✝)
h₁ : ∀ {m : ℕ}, m < Nat.succ n✝ → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
    Nat.rec (Part.some (Sum.inr a))
      (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
cases' h₁ (Nat.lt_succ_self _) with a' h
[GOAL]
case refine'_1.intro.intro.intro.succ.inl.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (Nat.succ n✝)
h₁ : ∀ {m : ℕ}, m < Nat.succ n✝ → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
    Nat.rec (Part.some (Sum.inr a))
      (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝
a' : α
h : Sum.inr a' ∈ F a n✝
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
injection mem_unique h h₂
[GOAL]
case refine'_1.intro.intro.intro.succ.inr.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (Nat.succ n✝)
h₁ : ∀ {m : ℕ}, m < Nat.succ n✝ → ∃ b, Sum.inr b ∈ F a m
a' : α
am' :
  Sum.inr a' ∈
    Nat.rec (Part.some (Sum.inr a))
      (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝
fa' : Sum.inl b ∈ f a'
⊢ b ∈ PFun.fix f a
[PROOFSTEP]
exact this _ _ am' (PFun.mem_fix_iff.2 (Or.inl fa'))
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
[PROOFSTEP]
suffices
  ∀ (a') (_ : b ∈ PFun.fix f a') (k) (_ : Sum.inr a' ∈ F a k),
    ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, ∀ (_ : k ≤ m), ∃ a₂, Sum.inr a₂ ∈ F a m
  by
  rcases this _ h 0 (by simp) with ⟨n, hn₁, hn₂⟩
  exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
this :
  ∀ (a' : α),
    b ∈ PFun.fix f a' →
      ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
[PROOFSTEP]
rcases this _ h 0 (by simp) with ⟨n, hn₁, hn₂⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
this :
  ∀ (a' : α),
    b ∈ PFun.fix f a' →
      ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ Sum.inr a ∈ F a 0
[PROOFSTEP]
simp
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
this :
  ∀ (a' : α),
    b ∈ PFun.fix f a' →
      ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ (m : ℕ), m < n → 0 ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
[PROOFSTEP]
exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
⊢ ∀ (a' : α),
    b ∈ PFun.fix f a' →
      ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
intro a₁ h₁
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
⊢ ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
apply @PFun.fixInduction _ _ _ _ _ _ h₁
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
⊢ ∀ (a' : α),
    b ∈ PFun.fix f a' →
      (∀ (a'' : α),
          Sum.inr a'' ∈ f a' →
            ∀ (k : ℕ),
              Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m) →
        ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
intro a₂ h₂ IH k hk
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)
[GOAL]
case refine'_2.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂✝ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
refine' ⟨k.succ, _, fun m mk km => ⟨a₂, _⟩⟩
[GOAL]
case refine'_2.inl.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂✝ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
⊢ Sum.inl b ∈ F a (Nat.succ k)
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inl.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂✝ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
⊢ Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a))
        (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) k ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) k ∧
        Sum.inl b ∈ f b_1
[PROOFSTEP]
exact Or.inr ⟨_, hk, h₂⟩
[GOAL]
case refine'_2.inl.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂✝ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < Nat.succ k
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a m
[PROOFSTEP]
rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
[GOAL]
case refine'_2.inr.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
rcases IH _ am₃ k.succ (by simp; exact ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
⊢ Sum.inr a₃ ∈ F a (Nat.succ k)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
⊢ ∃ b,
    Sum.inr b ∈
        Nat.rec (Part.some (Sum.inr a))
          (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) k ∧
      Sum.inr a₃ ∈ f b
[PROOFSTEP]
exact ⟨_, hk, am₃⟩
[GOAL]
case refine'_2.inr.intro.intro.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ (m : ℕ), m < n → Nat.succ k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
refine' ⟨n, hn₁, fun m mn km => _⟩
[GOAL]
case refine'_2.inr.intro.intro.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ (m : ℕ), m < n → Nat.succ k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km : k ≤ m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
cases' km.lt_or_eq_dec with km km
[GOAL]
case refine'_2.inr.intro.intro.intro.intro.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ (m : ℕ), m < n → Nat.succ k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km✝ : k ≤ m
km : k < m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
exact hn₂ _ mn km
[GOAL]
case refine'_2.inr.intro.intro.intro.intro.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ✝ : Type u_4
inst✝³ : Primcodable α✝
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ✝
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ PFun.fix f a
a₁ : α
h₁ : b ∈ PFun.fix f a₁
a₂ : α
h₂ : b ∈ PFun.fix f a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ (m : ℕ), m < n → k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ PFun.fix f a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ (m : ℕ), m < n → Nat.succ k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km✝ : k ≤ m
km : k = m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m
[PROOFSTEP]
exact km ▸ ⟨_, hk⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
⊢ Partrec (PFun.fix f)
[PROOFSTEP]
let F : α → ℕ →. Sum σ α := fun a n =>
  n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
⊢ Partrec (PFun.fix f)
[PROOFSTEP]
have hF : Partrec₂ F :=
  Partrec.nat_rec snd (sum_inr.comp fst).partrec
    (sum_casesOn_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
⊢ Partrec (PFun.fix f)
[PROOFSTEP]
let p a n := @Part.map _ Bool (fun s => Sum.casesOn s (fun _ => true) fun _ => false) (F a n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
⊢ Partrec (PFun.fix f)
[PROOFSTEP]
have hp : Partrec₂ p := hF.map ((sum_casesOn Computable.id (const true).to₂ (const false).to₂).comp snd).to₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
⊢ Partrec (PFun.fix f)
[PROOFSTEP]
exact
  (hp.rfind.bind (hF.bind (sum_casesOn_right snd snd.to₂ none.to₂).to₂).to₂).of_eq fun a =>
    ext fun b => by simp; apply fix_aux f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
a : α
b : σ
⊢ (b ∈
      Part.bind (Nat.rfind (p a)) fun b =>
        Part.bind (F (a, b).fst (a, b).snd) fun b_1 =>
          Sum.casesOn ((a, b), b_1).snd (fun b_2 => Part.some (((a, b), b_1), b_2).snd) fun b => Part.none) ↔
    b ∈ PFun.fix f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => Part.bind IH fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
a : α
b : σ
⊢ (∃ a_1,
      ((∃ a_2,
            Sum.inl a_2 ∈
              Nat.rec (Part.some (Sum.inr a))
                (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) a_1) ∧
          ∀ {m : ℕ},
            m < a_1 →
              ∃ b,
                Sum.inr b ∈
                  Nat.rec (Part.some (Sum.inr a))
                    (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) m) ∧
        Sum.inl b ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH => Part.bind IH fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) a_1) ↔
    b ∈ PFun.fix f a
[PROOFSTEP]
apply fix_aux f
