awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
b : β
⊢ (bif (encode (α := β ⊕ γ) (Sum.inl b)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)
    else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)) =
    Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inl b) (g a) (h a))

Tactic:
simp [Nat.div2_val]

Premises used: Nat.div2_val
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
c : γ
⊢ (bif (encode (α := β ⊕ γ) (Sum.inr c)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)
    else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)) =
    Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inr c) (g a) (h a))

Tactic:
simp [Nat.div2_val]

Premises used: Nat.div2_val
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
x : Fin 0 → α → σ
h : ∀ (i : Fin 0), Computable (x i)
⊢ Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ []

Tactic:
const []

Premises used: Computable.const, List.nil
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
x : Fin 0 → α → σ
h : ∀ (i : Fin 0), Computable (x i)
⊢ Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ []

Tactic:
exact const []

Premises used: Computable.const, List.nil
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
simp : Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ f 0 a :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ a
⊢ Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i a

Tactic:
simp only [List.ofFn_succ]

Premises used: List.ofFn_succ
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ f 0 a :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ a

Tactic:
list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Premises used: Computable.list_cons, Fin.succ, Computable₂.comp, OfNat.ofNat
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ f 0 a :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ a

Tactic:
exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Premises used: Computable.list_cons, Fin.succ, Computable₂.comp, OfNat.ofNat
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ Eq.{u_4 + 1} (α := Part (List.Vector σ n)) (Vector.mOfFn fun (i : Fin n) ↦ (↑(f i) : α →. σ) a)
    ((↑fun (a : α) ↦ List.Vector.ofFn fun (i : Fin n) ↦ f i a : α →. List.Vector σ n) a)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
h : Partrec.{u_1, u_4} (α := α) (σ := Option σ) fun (a : α) ↦ Part.map Option.some (f a)
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ←
        Part.bind (↑(decode n) : Part α) fun (a : α) ↦
            Part.map.{u_4, 0} (α := Option σ) encode ((fun (a : α) ↦ Part.map Option.some (f a)) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a))

Tactic:
simp [Part.bind_assoc, bind_some_eq_map]

Premises used: Part.bind_some_eq_map, Part.bind_assoc
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this :
  Partrec.{u_1, u_4} (α := α) (σ := σ) fun (a : α) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (o a)) (Part.some (f a)) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) (g a)
a : α
none :
  Eq.{u_4 + 1} (α := Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode.{u_2} (α := Option β) Option.none) (Part.some (f a))
        fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part β) (g a) :
      Part σ)
    (Option.casesOn (motive := fun (x : Option β) ↦ Part σ) Option.none (Part.some (f a)) (g a) : Part σ)
some :
  ∀ (b : β),
    Eq.{u_4 + 1} (α := Part σ)
      (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (Option.some b)) (Part.some (f a)) fun (n : ℕ) ↦
          Part.bind (↑(decode n) : Part β) (g a) :
        Part σ)
      (Option.casesOn (motive := fun (x : Option β) ↦ Part σ) (Option.some b) (Part.some (f a)) (g a) : Part σ)
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (o a)) (Part.some (f a)) fun (n : ℕ) ↦
        Part.bind (↑(decode n) : Part β) (g a) :
      Part σ)
    (Option.casesOn (motive := fun (x : Option β) ↦ Part σ) (o a) (Part.some (f a)) (g a) : Part σ)

Tactic:
rcases o a with - | b
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this :
  Partrec.{u_1, u_4} (α := α) (σ := σ) fun (a : α) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (o a)) (Part.some (f a)) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) (g a)
a : α
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode.{u_2} (α := Option β) Option.none) (Part.some (f a))
        fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part β) (g a) :
      Part σ)
    (Option.casesOn (motive := fun (x : Option β) ↦ Part σ) Option.none (Part.some (f a)) (g a) : Part σ)

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this :
  Partrec.{u_1, u_4} (α := α) (σ := σ) fun (a : α) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (o a)) (Part.some (f a)) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) (g a)
a : α
b : β
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (encode (Option.some b)) (Part.some (f a)) fun (n : ℕ) ↦
        Part.bind (↑(decode n) : Part β) (g a) :
      Part σ)
    (Option.casesOn (motive := fun (x : Option β) ↦ Part σ) (Option.some b) (Part.some (f a)) (g a) : Part σ)

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec.{u_1, u_4} (α := α) (σ := Option σ) fun (a : α) ↦
    Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
      (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (f a) (fun (x : β) ↦ Option.none) Option.some)
      (Part.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (f a) (fun (b : β) ↦ Option.some (g a b)) fun (x : γ) ↦
          Option.none))
      fun (c : γ) ↦ Part.map Option.some (h a c)
a : α
inl :
  ∀ (val : β),
    Eq.{u_4 + 1} (α := Part (Option σ))
      (Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (Sum.inl val) (fun (x : β) ↦ Option.none) Option.some)
          (Part.some
            (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (Sum.inl val) (fun (b : β) ↦ Option.some (g a b))
              fun (x : γ) ↦ Option.none))
          fun (c : γ) ↦ Part.map Option.some (h a c) :
        Part (Option σ))
      (Part.map Option.some
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (fun (b : β) ↦ Part.some (g a b)) (h a)) :
        Part (Option σ))
inr :
  ∀ (val : γ),
    Eq.{u_4 + 1} (α := Part (Option σ))
      (Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (Sum.inr val) (fun (x : β) ↦ Option.none) Option.some)
          (Part.some
            (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (Sum.inr val) (fun (b : β) ↦ Option.some (g a b))
              fun (x : γ) ↦ Option.none))
          fun (c : γ) ↦ Part.map Option.some (h a c) :
        Part (Option σ))
      (Part.map Option.some
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (fun (b : β) ↦ Part.some (g a b)) (h a)) :
        Part (Option σ))
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (f a) (fun (x : β) ↦ Option.none) Option.some)
        (Part.some
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (f a) (fun (b : β) ↦ Option.some (g a b)) fun (x : γ) ↦
            Option.none))
        fun (c : γ) ↦ Part.map Option.some (h a c) :
      Part (Option σ))
    (Part.map Option.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (f a) (fun (b : β) ↦ Part.some (g a b)) (h a)) :
      Part (Option σ))

Tactic:
cases f a
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec.{u_1, u_4} (α := α) (σ := Option σ) fun (a : α) ↦
    Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
      (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (f a) (fun (x : β) ↦ Option.none) Option.some)
      (Part.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (f a) (fun (b : β) ↦ Option.some (g a b)) fun (x : γ) ↦
          Option.none))
      fun (c : γ) ↦ Part.map Option.some (h a c)
a : α
val : β
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (Sum.inl val) (fun (x : β) ↦ Option.none) Option.some)
        (Part.some
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (Sum.inl val) (fun (b : β) ↦ Option.some (g a b))
            fun (x : γ) ↦ Option.none))
        fun (c : γ) ↦ Part.map Option.some (h a c) :
      Part (Option σ))
    (Part.map Option.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (fun (b : β) ↦ Part.some (g a b)) (h a)) :
      Part (Option σ))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec.{u_1, u_4} (α := α) (σ := Option σ) fun (a : α) ↦
    Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
      (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (f a) (fun (x : β) ↦ Option.none) Option.some)
      (Part.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (f a) (fun (b : β) ↦ Option.some (g a b)) fun (x : γ) ↦
          Option.none))
      fun (c : γ) ↦ Part.map Option.some (h a c)
a : α
val : γ
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (Option.casesOn (motive := fun (x : Option γ) ↦ Part (Option σ))
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option γ) (Sum.inr val) (fun (x : β) ↦ Option.none) Option.some)
        (Part.some
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Option σ) (Sum.inr val) (fun (b : β) ↦ Option.some (g a b))
            fun (x : γ) ↦ Option.none))
        fun (c : γ) ↦ Part.map Option.some (h a c) :
      Part (Option σ))
    (Part.map Option.some
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (fun (b : β) ↦ Part.some (g a b)) (h a)) :
      Part (Option σ))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
inl :
  ∀ (val : β),
    Eq.{u_4 + 1} (α := Part σ)
      (Sum.casesOn (motive := fun (x : γ ⊕ β) ↦ Part σ)
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ γ ⊕ β) (Sum.inl val) (fun (b : β) ↦ Sum.inr (a, b).2) fun (b : γ) ↦
            Sum.inl (a, b).2)
          (fun (b : γ) ↦ Part.some (h a b)) (g a) :
        Part σ)
      (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) fun (c : γ) ↦ Part.some (h a c) : Part σ)
inr :
  ∀ (val : γ),
    Eq.{u_4 + 1} (α := Part σ)
      (Sum.casesOn (motive := fun (x : γ ⊕ β) ↦ Part σ)
          (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ γ ⊕ β) (Sum.inr val) (fun (b : β) ↦ Sum.inr (a, b).2) fun (b : γ) ↦
            Sum.inl (a, b).2)
          (fun (b : γ) ↦ Part.some (h a b)) (g a) :
        Part σ)
      (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (g a) fun (c : γ) ↦ Part.some (h a c) : Part σ)
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Sum.casesOn (motive := fun (x : γ ⊕ β) ↦ Part σ)
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ γ ⊕ β) (f a) (fun (b : β) ↦ Sum.inr (a, b).2) fun (b : γ) ↦
          Sum.inl (a, b).2)
        (fun (b : γ) ↦ Part.some (h a b)) (g a) :
      Part σ)
    (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (f a) (g a) fun (c : γ) ↦ Part.some (h a c) : Part σ)

Tactic:
cases f a
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val : β
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Sum.casesOn (motive := fun (x : γ ⊕ β) ↦ Part σ)
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ γ ⊕ β) (Sum.inl val) (fun (b : β) ↦ Sum.inr (a, b).2) fun (b : γ) ↦
          Sum.inl (a, b).2)
        (fun (b : γ) ↦ Part.some (h a b)) (g a) :
      Part σ)
    (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) fun (c : γ) ↦ Part.some (h a c) : Part σ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val : γ
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Sum.casesOn (motive := fun (x : γ ⊕ β) ↦ Part σ)
        (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ γ ⊕ β) (Sum.inr val) (fun (b : β) ↦ Sum.inr (a, b).2) fun (b : γ) ↦
          Sum.inl (a, b).2)
        (fun (b : γ) ↦ Part.some (h a b)) (g a) :
      Part σ)
    (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (g a) fun (c : γ) ↦ Part.some (h a c) : Part σ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 ∈ f.fix a

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
refine_1 :
  ∀
    (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 ∈ f.fix a
refine_2 :
  ∀ (h : b ∈ f.fix 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
⊢ (∃ (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 ∈ f.fix a

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
refine_1 :
  ∀ (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 ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
a' : α
am : Sum.inr a' ∈ F a 0
ba : b ∈ f.fix a'
⊢ a' = a

Tactic:
simp [F] at am
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
a' : α
ba : b ∈ f.fix a'
am : a' = a
zero zero₁ zero₂ zero₃ : b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
rwa [← am]
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a
a' : α
am : Sum.inr a' ∈ F a (m + 1)
ba : b ∈ f.fix a'
⊢ ∃ (b : α),
    Membership.mem (γ := Part (σ ⊕ α))
        (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
            (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
              IH.bind fun (s : σ ⊕ α) ↦
                Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                  s)
            m :
          Part (σ ⊕ α))
        (Sum.inr b) ∧
      Sum.inr a' ∈ f b

Tactic:
simp [F] at am
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
am :
  ∃ (b : α),
    Membership.mem (γ := Part (σ ⊕ α))
        (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
            (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
              IH.bind fun (s : σ ⊕ α) ↦
                Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                  s)
            m :
          Part (σ ⊕ α))
        (Sum.inr b) ∧
      Sum.inr a' ∈ f b
succ :
  ∀ (a₂ : α)
    (am₂ :
      Membership.mem (γ := Part (σ ⊕ α))
        (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
            (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
              IH.bind fun (s : σ ⊕ α) ↦
                Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                  s)
            m :
          Part (σ ⊕ α))
        (Sum.inr a₂))
    (fa₂ : Sum.inr a' ∈ f a₂), b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
rcases am with ⟨a₂, am₂, fa₂⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
a₂ : α
am₂ :
  Membership.mem (γ := Part (σ ⊕ α))
    (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
        (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
          IH.bind fun (s : σ ⊕ α) ↦
            Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val) s)
        m :
      Part (σ ⊕ α))
    (Sum.inr a₂)
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ f.fix a

Tactic:
IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff, Or.inr
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
a₂ : α
am₂ :
  Membership.mem (γ := Part (σ ⊕ α))
    (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
        (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
          IH.bind fun (s : σ ⊕ α) ↦
            Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val) s)
        m :
      Part (σ ⊕ α))
    (Sum.inr a₂)
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ f.fix a

Tactic:
exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff, Or.inr