awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
have hx₁ : a' = x
Tactic: simp only [encodek, Option.some_inj] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
have hx₁ : a' = x
Tactic: simp only [encodek, Option.some_inj] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
have ha₁ : x ∈ f a
Tactic: rw [hx] at ha
Cleared hypotheses: ha, hn, hx
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
have ha₁ : x ∈ g a
Tactic: rw [hx] at ha
Cleared hypotheses: ha, hn, hx
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
⊢ (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
have this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
Tactic: have : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a := by
    intro x h'
    simp only [k', mem_coe, mem_bind_iff, Option.mem_def] at h'
    obtain ⟨n, hn, hx⟩ := h'
    have := (H _).1 _ hn
    simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this
    obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this <;> simp only [encodek, Option.some_inj] at hx <;>
      rw [hx] at ha
    · exact Or.inl ha
    · exact Or.inr ha
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
⊢ (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
have refine : (f a).Dom ∨ (g a).Dom → (k' a).Dom
Tactic: refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom
have rw : ∃ (h : (k (encode a)).Dom), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get h)) : Part σ)
Tactic: rw [bind_dom]
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ (h : (k (encode a)).Dom), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get h)) : Part σ)
have hk₁ : (k (encode a)).Dom
Tactic: have hk : (k (encode a)).Dom :=
    (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] using h)
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∃ (h : (k (encode a)).Dom), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get h)) : Part σ)
have exists : Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
Tactic: exists hk
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
have H₁ : ∀ (a : ℕ),
  (∀ x ∈ k a,
      (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
        ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
    ((k a).Dom ↔
      Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
Tactic: simp only [mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
have inl : ∀ (a' : α),
  decode₂ α (encode a) = Option.some a' →
    ∀ y ∈ f a',
      ∀ (e : encode y = (k (encode a)).get hk), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
Tactic: obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
inl :
  ∀ (a' : α),
    decode₂ α (encode a) = Option.some a' →
      ∀ y ∈ f a',
        ∀ (e : encode y = (k (encode a)).get hk), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
have inr : ∀ (a' : α),
  decode₂ α (encode a) = Option.some a' →
    ∀ y ∈ g a',
      ∀ (e : encode y = (k (encode a)).get hk), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
Tactic: obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
⊢ x ∈ k a
have this : (k a).Dom
Tactic: have : (k a).Dom := (K _).2.2 (h.imp Exists.fst Exists.fst)
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ x ∈ k a
have refine : (k a).get this = x
Tactic: refine ⟨this, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ (k a).get this = x
have inl : ∀ (h : x ∈ f a), (k a).get this = x
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
inl : ∀ (h : x ∈ f a), (k a).get this = x
⊢ (k a).get this = x
have inr : ∀ (h : x ∈ g a), (k a).get this = x
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
⊢ (k a).get this = x
have inl : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
Tactic: rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
inl : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
⊢ (k a).get this = x
have inl₁ : ∀ (h' : (k a).get this ∈ g a), (k a).get this = x
Tactic: rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
⊢ (k a).get this = x
have inr : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
Tactic: rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
inr : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
⊢ (k a).get this = x
have inr₁ : ∀ (h' : (k a).get this ∈ g a), (k a).get this = x
Tactic: rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a)
cg : Code
eg : cg.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a)
a : α
⊢ (((bif c a then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif c a then f a else g a
have false : (((bif false then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
  bif false then f a else g a
Tactic: cases c a
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a)
cg : Code
eg : cg.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a)
a : α
false :
  (((bif Bool.false then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif Bool.false then f a else g a
⊢ (((bif c a then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif c a then f a else g a
have true : (((bif true then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
  bif true then f a else g a
Tactic: cases c a
-- Lean 4 proof step from Mathlib.Computability.RE (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 : Partrec₂ h
a : α
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (f a) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (f a) (g a) (h a)) : Part (Option σ))
have inl : ∀ (val : β),
  Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inl val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) (h a)) :
      Part (Option σ))
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.RE (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 : Partrec₂ h
a : α
inl :
  ∀ (val : β),
    Eq.{u_4 + 1} (α := Part (Option σ))
      (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inl val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val)
            (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
        else
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val) (fun (b : β) ↦ Part.some Option.none)
            fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
        Part (Option σ))
      (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) (h a)) :
        Part (Option σ))
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (f a) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (f a) (g a) (h a)) : Part (Option σ))
have inr : ∀ (val : γ),
  Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inr val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (g a) (h a)) :
      Part (Option σ))
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
⊢ Computable (σ := ℕ) fun (x : α) ↦ Nat.find (p := P x) ⋯
have h : Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
Tactic: have h : Partrec (fun x ↦ Nat.rfind fun n => Part.some (decide (P x n))) :=
    Partrec.rfind hP_comp.decide.partrec
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
h : Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
⊢ Computable (σ := ℕ) fun (x : α) ↦ Nat.find (p := P x) ⋯
have refine : ∀ (x : α), Nat.find (p := P x) sorry ∈ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
Tactic: refine h.of_eq_tot fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
hp : ComputablePred p
⊢ REPred p
have obtain : ∀ (f : α → Bool) (hf : Computable f) (hp : ComputablePred fun (a : α) ↦ f a = true), REPred fun (a : α) ↦ f a = true
Tactic: obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
Cleared hypotheses: p, hp