calc
  (S₁ + S₂ * p){L}[i] = (S₁ + p * S₂) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1         := by simp [ext, mul_comm S₂]
  _                   = (S₁ + bexp (S₁ + S₂ * p) (i * ‖L‖) * (L # 1 * q * S₂)) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1 := by simp [←mul_assoc, ←hq]
  _                   = (S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) + L # 1 * q * S₂) % L # 1 := by rw [div_add_mul_self' _ _ (bexp_pos lt_len)]
  _                   = S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1                    := by simp [mul_assoc]
  _                   = S₁{L}[i]                                                     := ext_eq_of_ge le_self_add
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
no goals