have : x < a := exp_monotone.mp <| LE.le.trans_lt (exp_le_of_mem hx) hs
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
⊢ x ∈ b
case intro.h.mpr
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
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
this : x < a
⊢ x ∈ b