refine ⟨‖S‖, by simp, rfl, ‖L‖, by simp, rfl, ?_⟩
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ ∃ lS ≤ S,
    lS = ‖S‖ ∧
      ∃ lL ≤ L,
        lL = ‖L‖ ∧
          (lS ≤ i * lL → S / b % L # 1 = 0) ∧
            (i * lL < lS →
              ∃ b_1 ≤ S,
                Exponential (i * lL) b_1 ∧
                  ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)
case inr.mp.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‖
b : M
hb : b ≤ S
Hb : Exponential (i * ‖L‖) b
⊢ (‖S‖ ≤ i * ‖L‖ → S / b % L # 1 = 0) ∧
    (i * ‖L‖ < ‖S‖ →
      ∃ b_1 ≤ S,
        Exponential (i * ‖L‖) b_1 ∧
          ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b_1 ∧ S / b % L # 1 = divS % hL)