rcases this with ⟨s, hsn, hs⟩
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
this : ∃ s < exp a, ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i