MeasureTheory.simplify_factor_aux₄

lemma simplify_factor_aux₄ [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (hq₀' : q₀ ≠ ⊤)    (hp₀ : p₀ ∈ Ioc 0 q₀) (ht : t ∈ Ioo 0 1)    (hp₀p₁ : p₀ = p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :    ↑C₀ ^ ((1 - t).toReal * q.toReal) * (eLpNorm f p μ ^ p.toReal) ^ ((1 - t).toReal * p₀⁻¹.toReal * q.toReal) *      ↑C₁ ^ (t.toReal * q.toReal) *    (eLpNorm f p μ ^ p.toReal) ^ (t.toReal * p₁⁻¹.toReal * q.toReal) = C₀ ^ ((1 - t).toReal * q.toReal) *    C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal := by  have hp' : p₀ = p := (interp_exp_eq hp₀p₁ ht hp)  have p₀ne_top : p₀ ≠ ⊤ := ne_top_of_le_ne_top hq₀' hp₀.2  have p₀toReal_pos : 0 < p₀.toReal := toReal_pos hp₀.1.ne' p₀ne_top  rw [← hp', ← hp₀p₁]  have (a b c d : ℝ≥0∞): a * b * c * d = a * c * (b * d) := by ring  rw [this, ← ENNReal.rpow_add]  · rw [← ENNReal.rpow_mul]    congr    rw [toReal_inv]    ring_nf    field_simp    have : (1 - t + t).toReal = 1 := by      rw [toReal_eq_one_iff, add_comm, add_tsub_cancel_iff_le]      exact ht.2.le    rw [mul_comm, ← toReal_add, this, one_mul]    · finiteness    · finiteness  · exact hp' ▸ d_pos_aux₀ hF |>.ne'  · exact hp' ▸ d_ne_top_aux₀ hF