have : y < y := calc
  y < 2 * z := hyz
  _ ≤ z'    := (Pow2.lt_iff_two_mul_le H.range_pow2 H'.range_pow2).mp this
  _ ≤ y     := hzy'
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'
this : z < 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'
this✝ : z < z'
this : y < y
⊢ False