ComputationsInterpolatedExponents.interp_exp_between

lemma interp_exp_between (hp₀ : 0 < p₀) (hp₁ : 0 < p₁)    (hp₀p₁ : p₀ < p₁) (ht : t ∈ Ioo 0 1)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p ∈ Ioo p₀ p₁ := by  have ht' : t ≠ ∞ := (ht.2.trans one_lt_top).ne  refine ⟨?_, ?_⟩ <;> apply ENNReal.inv_lt_inv.mp  · rw [hp]    have : p₀⁻¹ = (1 - t) * p₀⁻¹ + t * p₀⁻¹ := by      rw [← add_mul, tsub_add_eq_max, max_eq_left_of_lt, one_mul]      exact ht.2    nth_rw 2 [this]    gcongr    · finiteness    · exact ht.1.ne'  · rw [hp]    have : p₁⁻¹ = (1 - t) * p₁⁻¹ + t * p₁⁻¹ := by      rw [← add_mul, tsub_add_eq_max, max_eq_left_of_lt, one_mul]      exact ht.2    nth_rw 1 [this]    gcongr    · finiteness    · exact (tsub_pos_iff_lt.mpr ht.2).ne'    · exact (mem_sub_Ioo (one_ne_top) ht).2.trans one_lt_top |>.ne