ComputationsChoiceExponent.eq_exponents₃

lemma eq_exponents₃ (ht : t ∈ Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :    (p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal)) * (q.toReal - q₀.toReal) =      - t.toReal * p₁⁻¹.toReal * q.toReal := by  rw [mul_comm_div, ← mul_div_assoc]  have : (p₁⁻¹.toReal * q₀⁻¹.toReal) * (q.toReal - q₀.toReal) =      - t.toReal * p₁⁻¹.toReal * q.toReal * (q₁⁻¹.toReal - q₀⁻¹.toReal) := by    calc    _ = p₁⁻¹.toReal * (q₀⁻¹.toReal * q.toReal - q₀⁻¹.toReal * q₀.toReal) := by ring    _ = p₁⁻¹.toReal * (q₀⁻¹.toReal * q.toReal - 1) := by      rw [toReal_inv, toReal_inv, inv_mul_cancel₀]      apply (exp_toReal_pos hq₀ hq₀').ne'    _ = p₁⁻¹.toReal * (q₀⁻¹.toReal * q.toReal - q⁻¹.toReal * q.toReal) := by      rw [toReal_inv, toReal_inv, toReal_inv, inv_mul_cancel₀]      exact (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq).ne'    _ = p₁⁻¹.toReal * q.toReal * (q₀⁻¹.toReal - q⁻¹.toReal) := by ring    _ = _ := by      rw [preservation_interpolation ht hq₀ hq₁ hq, one_sub_ioo_toReal ht]      ring  rw [this, mul_div_cancel_right₀]  exact ne_sub_toReal_exp hq₀ hq₁ hq₀q₁