ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp

lemma ne_inv_toReal_exp_interp_exp (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀⁻¹.toReal ≠ p⁻¹.toReal := by  rw [preservation_interpolation ht hp₀ hp₁ hp, ← sub_ne_zero]  convert mul_ne_zero (toReal_ne_zero_of_Ioo ht)    (sub_ne_zero_of_ne (ne_inv_toReal_exponents hp₀ hp₁ hp₀p₁)) using 1  -- These lines used to be  -- rw [ENNReal.sub_mul, one_mul, add_comm_sub, sub_add_eq_sub_sub, sub_self, zero_sub,  -- neg_sub, ← _root_.mul_sub]  rw [mul_sub, tsub_add_eq_tsub_tsub]  nth_rw 1 [← one_mul p₀⁻¹.toReal]  have : (1 - t) + t = 1 := by rw [tsub_add_cancel_iff_le]; exact ht.2.le  rw [← sub_mul]  congr  rw [sub_eq_iff_eq_add', ← toReal_add (by finiteness) (by finiteness), this, ← ENNReal.toReal_one]