Theorem: Partrec.merge_iff (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
Tactic:
rcases merge hf hg H with ⟨k, _, hk⟩
State after:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
k : α →. σ
left✝ : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a

State before:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
k : α →. σ
left✝ : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
Tactic:
exact Classical.epsilon_spec (p := fun k => ∀ a x, x ∈ k a ↔ x ∈ f a ∨ x ∈ g a) ⟨k, hk⟩ a x
State after:
no goals