rcases this.mp H' with ⟨y, _, rfl, H''⟩
case intro.inr.mp.intro.intro
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' : Exponential (x + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this✝¹ : Exponential (2 * (x + 1)) (y ^ 2)
this✝ : 1 < y
this : Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z
⊢ ∃ z ≤ y ^ 2, y ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z
case intro.inr.mp.intro.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 ⊧ₘ* 𝐈𝚫₀
x y : M
H'' : Exponential x y
H' : Exponential (x + 1) (2 * y)
IH : ∀ y_1 < (2 * y) ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < (2 * y) ^ 2
H : Exponential (2 * x + 1 + 1) ((2 * y) ^ 2)
this✝¹ : Exponential (2 * (x + 1)) ((2 * y) ^ 2)
this✝ : 1 < 2 * y
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
left✝ : y ≤ 2 * y
⊢ ∃ z ≤ (2 * y) ^ 2, (2 * y) ^ 2 = 2 * z ∧ Exponential (2 * x + 1) z