have : b < b := calc
  b < 2 * b' := hb
  _ ≤ a'     := (Pow2.lt_iff_two_mul_le Hb.range_pow2 Ha.range_pow2).mp this
  _ ≤ a      := ha'
  _ ≤ b      := h
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this : b' < a'
⊢ False
case inr.inr.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 ⊧ₘ* 𝐈𝚫₀
a b : M
h : a ≤ b
posa : 0 < a
posb : 0 < b
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
right✝ : a < 2 * a'
b' : M
left✝ : b' ≤ b
Hb : Exponential (log b) b'
hb : b < 2 * b'
lt : ¬log a ≤ log b
this✝ : b' < a'
this : b < b
⊢ False