ComputationsInterpolatedExponents.exp_gt_iff

lemma exp_gt_iff (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) :    p₀ < p ↔ p₀ < p₁ := by  rcases lt_or_gt_of_ne hp₀p₁ with p₀lt_p₁ | p₁lt_p₀  · exact ⟨fun _ ↦ p₀lt_p₁, fun _ ↦ (interp_exp_between hp₀ hp₁ p₀lt_p₁ ht hp).1⟩  · exact ⟨fun h ↦ (not_le_of_gt h (interp_exp_between hp₁ hp₀ p₁lt_p₀      (mem_sub_Ioo one_ne_top ht) (switch_exponents ht hp)).2.le).elim,      fun h ↦ (not_le_of_gt h p₁lt_p₀.le).elim⟩