exact ⟨b, hb, Hb, by rw [HhL.uniq (exponential_hash_one L)]⟩
case inr.mpr.intro.intro.intro.intro.intro.intro.intro.intro.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
lt : i * ‖L‖ < ‖S‖
left✝⁴ : ‖S‖ ≤ S
left✝³ : ‖L‖ ≤ L
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
hL : M
left✝² : hL ≤ 2 * L + 1
HhL : Exponential ‖L‖ hL
left✝¹ : S / b ≤ S
left✝ : ‖S‖ ≤ i * ‖L‖ → S / b % hL = 0
h :
  i * ‖L‖ < ‖S‖ →
    ∃ b_1 ≤ S,
      Exponential (i * ‖L‖) b_1 ∧
        ∃ hL_1 ≤ 2 * L + 1, Exponential ‖L‖ hL_1 ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % hL = divS % hL_1
⊢ ∃ b_1 ≤ S, Exponential (i * ‖L‖) b_1 ∧ S / b % hL = S / b_1 % L # 1
no goals