MeasureTheory.C_realInterpolation_ENNReal_ne_top

lemma C_realInterpolation_ENNReal_ne_top {p₀ p₁ q₀ q₁ q : ℝ≥0∞} {A : ℝ≥0}    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) :    C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t ≠ ⊤ := by  have q₀pos : 0 < q₀ := pos_of_rb_Ioc hp₀  have q₁pos : 0 < q₁ := pos_of_rb_Ioc hp₁  unfold C_realInterpolation_ENNReal  apply mul_ne_top  · apply mul_ne_top    · apply mul_ne_top      · finiteness [interpolated_pos' q₀pos q₁pos (ne_top_of_Ioo ht) hq |>.ne',          interp_exp_ne_top hq₀q₁ ht hq]      · apply rpow_ne_top'        · split_ifs          · rw [one_mul, one_mul]            apply ne_of_gt            apply add_pos'            · exact ofReal_inv_interp_sub_exp_pos₁ ht q₀pos q₁pos hq₀q₁ hq            · exact ofReal_inv_interp_sub_exp_pos₀ ht q₀pos q₁pos hq₀q₁ hq          · simp [ofReal_inv_interp_sub_exp_pos₁ ht q₀pos q₁pos hq₀q₁ hq |>.ne']          · simp [ofReal_inv_interp_sub_exp_pos₀ ht q₀pos q₁pos hq₀q₁ hq |>.ne']          · simp_all        · split_ifs <;> exact (ne_of_beq_false rfl).symm    · finiteness  · finiteness