α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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 : (k a).Dom := (K _).2.2 (h.imp Exists.fst Exists.fst)
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
⊢ Part.get (k a) this = x
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
refine' ⟨this, _⟩
case inl.inl
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x

case inl.inr
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x

case inr.inl
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x

case inr.inr
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
⊢ Part.get (k a) this = x
cases' h with h h <;> cases' (K _).1 _ ⟨this, rfl⟩ with h' h'
no goals
case inl.inl
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x
exact mem_unique h' h
no goals
case inl.inr
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x
exact (H _ _ h _ h').symm
no goals
case inr.inl
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x
exact H _ _ h' _ h
no goals
case inr.inr
α : Type u_1
β : Type ?u.258088
γ : Type ?u.258091
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), 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
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x
exact mem_unique h' h