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₀ ≠ ⊤) :    (q₀.toReal / p₀.toReal + p₀⁻¹.toReal * q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) *      (q.toReal - q₀.toReal)) = (1 - t).toReal * p₀⁻¹.toReal * q.toReal := by  rw [div_eq_inv_mul, mul_div_assoc, mul_assoc, toReal_inv, ← mul_add, mul_comm_div,    ← mul_div_assoc, add_div']  · have : q₀.toReal * (q₁⁻¹.toReal - q₀⁻¹.toReal) + q₁⁻¹.toReal * (q.toReal - q₀.toReal) =        q.toReal * ((1 - t).toReal * (q₁⁻¹.toReal - q₀⁻¹.toReal)) := by      calc      _ = q₀.toReal * q₁⁻¹.toReal - q₀.toReal * q₀⁻¹.toReal +          q₁⁻¹.toReal * q.toReal - q₁⁻¹.toReal *  q₀.toReal := by        ring      _ = q₁⁻¹.toReal * q.toReal - q⁻¹.toReal * q.toReal := by        rw [toReal_inv, toReal_inv, toReal_inv, mul_inv_cancel₀, inv_mul_cancel₀]        · ring        · exact (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq).ne'        · exact (toReal_pos hq₀.ne' hq₀').ne'      _ = q.toReal * (q₁⁻¹.toReal - q⁻¹.toReal) := by ring      _ = _ := by        rw [preservation_interpolation ht hq₀ hq₁ hq]        congr        rw [one_sub_ioo_toReal ht]        ring    rw [this, mul_div_assoc, mul_div_cancel_right₀]    · ring    · exact ne_sub_toReal_exp hq₀ hq₁ hq₀q₁  · exact ne_sub_toReal_exp hq₀ hq₁ hq₀q₁