rcases hx' with ⟨_, z', hzy', H', _⟩
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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
hx' : x' < y ∧ ∃ y' ≤ y, Exponential x' y' ∧ y < 2 * y'
A : ¬x' = x
lt : x < x'
left✝¹ : x < y
z : M
left✝ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
⊢ False
case intro.intro.intro.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✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x x' : M
A : ¬x' = x
lt : x < x'
left✝² : x < y
z : M
left✝¹ : z ≤ y
H : Exponential x z
hyz : y < 2 * z
left✝ : x' < y
z' : M
hzy' : z' ≤ y
H' : Exponential x' z'
right✝ : y < 2 * z'
⊢ False