α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
let k' (a : α) := (k (encode a)).bind fun n => (decode (α := σ) n : Part σ)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
refine'
  ⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂,
    fun a => _⟩
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ?m.252193
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ?m.252193
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
suffices
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom

case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ?m.252193
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ?m.252193
refine' ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩
case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a
case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
intro x h'
case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : ∃ a_1, a_1 ∈ k (encode a) ∧ decode a_1 = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a
simp only [exists_prop, mem_coe, mem_bind_iff, Option.mem_def] at h'
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
case this
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : ∃ a_1, a_1 ∈ k (encode a) ∧ decode a_1 = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
obtain ⟨n, hn, hx⟩ := h'
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (f a)) ∨
    n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
have := (H _).1 _ hn
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1, a_1 ∈ f a ∧ encode a_1 = n) ∨ ∃ a_1, a_1 ∈ g a ∧ encode a_1 = n
⊢ x ∈ f a ∨ x ∈ g a
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (f a)) ∨
    n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a
simp [mem_decode₂, encode_injective.eq_iff] at this
case this.intro.intro.inl.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

case this.intro.intro.inr.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
case this.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1, a_1 ∈ f a ∧ encode a_1 = n) ∨ ∃ a_1, a_1 ∈ g a ∧ encode a_1 = n
⊢ x ∈ f a ∨ x ∈ g a
obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this <;> simp only [encodek, Option.some_inj] at hx <;>
  rw [hx] at ha
no goals
case this.intro.intro.inr.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
exact Or.inr ha
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom
intro h
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom
rw [bind_dom]
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
have hk : (k (encode a)).Dom :=
  (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] using h)
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
exists hk
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ f a_2 ∧ encode a = x) ∨
            ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ g a_2 ∧ encode a = x) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
simp only [exists_prop, mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H
no goals
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ f a_2 ∧ encode a = x) ∨
            ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ g a_2 ∧ encode a = x) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩ <;>
  simp only [e.symm, encodek, coe_some, some_dom]
no goals
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (f a)).Dom ∨
    (Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (g a)).Dom
simpa only [encodek₂, bind_some, coe_some] using h
no goals
case this.intro.intro.inl.intro.intro
α : Type u_1
β : Type ?u.251017
γ : Type ?u.251020
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
exact Or.inl ha