exact ExistsUnique.intro s H (fun s' H' ↦ mem_ext <| fun i ↦ by simp [H, H'])
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
no goals