awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : α) ↦ List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i a
have simp : Computable.{u_1, u_4} (σ := List σ) fun (a : α) ↦ f 0 a :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ a
Tactic: simp only [List.ofFn_succ]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 (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 σ)
have 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 σ)
Tactic: rcases o a with - | b
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 σ)
⊢ 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 σ)
have 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 σ)
Tactic: rcases o a with - | b
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : α
⊢ 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 σ))
have 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 σ))
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 σ))
⊢ 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 σ))
have 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 σ))
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : α
⊢ 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 σ)
have 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 σ)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 σ)
⊢ 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 σ)
have 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 σ)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
have 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
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ (∃ (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
have 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
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ b ∈ f.fix a
have 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
Tactic: rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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'
⊢ b ∈ f.fix a
have am₁ : a' = a
Tactic: simp [F] at am
Cleared hypotheses: am
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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 ∈ f.fix a
have 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
Tactic: simp [F] at am
Cleared hypotheses: am
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ b ∈ f.fix a
have 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
Tactic: rcases am with ⟨a₂, am₂, fa₂⟩
Cleared hypotheses: am
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
⊢ b ∈ f.fix a
have zero : ∀ (a' : α) (am : Sum.inr a' ∈ F a 0) (ba : b ∈ f.fix a'), b ∈ f.fix a
Tactic: induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
Cleared hypotheses: m, a', am, ba
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
zero : ∀ (a' : α) (am : Sum.inr a' ∈ F a 0) (ba : b ∈ f.fix a'), b ∈ f.fix a
⊢ b ∈ f.fix a
have zero₁ : ∀ (a' : α) (ba : b ∈ f.fix a') (am : a' = a), b ∈ f.fix a
Tactic: induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
Cleared hypotheses: m, a', am, ba
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
zero : ∀ (a' : α) (am : Sum.inr a' ∈ F a 0) (ba : b ∈ f.fix a'), b ∈ f.fix a
zero₁ : ∀ (a' : α) (ba : b ∈ f.fix a') (am : a' = a), b ∈ f.fix a
⊢ b ∈ f.fix a
have succ : ∀ (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 ∈ f.fix a
Tactic: induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
Cleared hypotheses: m, a', am, ba
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
zero : ∀ (a' : α) (am : Sum.inr a' ∈ F a 0) (ba : b ∈ f.fix a'), b ∈ f.fix a
zero₁ : ∀ (a' : α) (ba : b ∈ f.fix a') (am : a' = a), b ∈ f.fix a
succ :
  ∀ (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 ∈ f.fix a
⊢ b ∈ f.fix a
have succ₁ : ∀ (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),
  b ∈ f.fix a
Tactic: induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
Cleared hypotheses: m, a', am, ba
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ b ∈ f.fix a
have this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
Tactic: 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 generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
⊢ b ∈ f.fix a
have refine_1 : ∀ (h₂ : Sum.inl b ∈ F a 0) (_x : ∃ (b' : σ), Sum.inl b' ∈ F a 0) (h₁ : ∀ {m : ℕ}, m < 0 → ∃ (b : α), Sum.inr b ∈ F a m),
  b ∈ f.fix a
Tactic: cases n
Cleared hypotheses: n, h₂, _x, h₁
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
refine_1 :
  ∀ (h₂ : Sum.inl b ∈ F a 0) (_x : ∃ (b' : σ), Sum.inl b' ∈ F a 0)
    (h₁ : ∀ {m : ℕ}, m < 0 → ∃ (b : α), Sum.inr b ∈ F a m), b ∈ f.fix a
⊢ b ∈ f.fix a
have refine_1₁ : ∀ (n : ℕ) (h₂ : Sum.inl b ∈ F a (n + 1)) (_x : ∃ (b' : σ), Sum.inl b' ∈ F a (n + 1))
  (h₁ : ∀ {m : ℕ}, m < n + 1 → ∃ (b : α), Sum.inr b ∈ F a m), b ∈ f.fix a
Tactic: cases n
Cleared hypotheses: n, h₂, _x, h₁