rintro x ⟨v, hv, u, hu, rfl⟩
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), (∃ v ∈ s, ∃ u ∈ a, i = v ⁀' u) → i < log s + exp ((2 * log s + log a + 1) ^ 2) + 1
case intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a : M
this : 𝚺₁-Predicate fun x => ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
v : M
hv : v ∈ s
u : M
hu : u ∈ a
⊢ v ⁀' u < log s + exp ((2 * log s + log a + 1) ^ 2) + 1