-- Mathlib/Computability/Halting.lean
theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
    ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a :=
  ⟨fun h => ⟨h.to_re, h.not.to_re⟩, fun ⟨h₁, h₂⟩ =>
    ⟨‹_›, by
      obtain ⟨k, pk, hk⟩ :=
        Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
        (by
          intro a x hx y hy
          simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy
          cases hy.1 hx.1)
      refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_
      rw [hk]
      simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
      apply Decidable.em⟩⟩

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
a : α
x y : Bool
hx : p a ∧ true = x
hy : ¬p a ∧ false = y
⊢ x = y

Tactic:
cases hy.1 hx.1

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ p n ∨ ¬p n

Tactic:
apply Decidable.em

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
⊢ Computable fun a => decide (p a)

Tactic:
obtain ⟨k, pk, hk⟩ :=
  Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
  (by
    intro a x hx y hy
    simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
      and_true, exists_const] at hx hy
    cases hy.1 hx.1)

Result:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ Computable fun a => decide (p a)

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
a : α
x : Bool
hx : x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ())
y : Bool
hy : y ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ x = y

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
  and_true, exists_const] at hx hy

Result:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
a : α
x y : Bool
hx : p a ∧ true = x
hy : ¬p a ∧ false = y
⊢ x = y

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ Computable fun a => decide (p a)

Tactic:
refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_

Result:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ k n

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ k n

Tactic:
rw [hk]

Result:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ Part.map (fun b => true) (Part.assert (p n) fun x => Part.some ()) ∨
    (fun a => decide (p a)) n ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) n) fun x => Part.some ())

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ Part.map (fun b => true) (Part.assert (p n) fun x => Part.some ()) ∨
    (fun a => decide (p a)) n ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) n) fun x => Part.some ())

Tactic:
simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
  true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]

Result:
case intro.intro
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ p n ∨ ¬p n

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
⊢ ∀ (a : α),
    ∀ x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()),
      ∀ y ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ()), x = y

Tactic:
intro a x hx y hy

Result:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a => ¬p a
h₁ : REPred p
h₂ : REPred fun a => ¬p a
a : α
x : Bool
hx : x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ())
y : Bool
hy : y ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ x = y