simp [under] at this ⊢
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
this : (fun x => x - 1) (y + 1) = (fun x => x - 1) (exp x)
⊢ y = under x
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y : M
h : y + 1 = exp x
this : y = exp x - 1
⊢ y = exp x - 1