ComputationsChoiceExponent.ζ_equality₃

lemma ζ_equality₃ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁)    (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤)    (hq₀' : q₀ ≠ ⊤) :    ζ p₀ q₀ p₁ q₁ t.toReal = (p₀.toReal * (q₀.toReal - q.toReal))  / (q₀.toReal * (p₀.toReal - p.toReal)) := by  rw [ζ_equality₁ ht, ← preservation_interpolation, ← preservation_interpolation]  have q_pos : 0 < q := interpolated_pos' hq₀ hq₁ (ne_top_of_Ioo ht) hq  have p_pos : 0 < p := interpolated_pos' hp₀ hp₁ (ne_top_of_Ioo ht) hp  have aux := mul_pos (interp_exp_toReal_pos ht hp₀ hp₁ hp₀p₁ hp)    (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq)  have hne : 0 < p.toReal * q.toReal * p₀.toReal * q₀.toReal :=    mul_pos (mul_pos aux (exp_toReal_pos hp₀ hp₀')) (exp_toReal_pos hq₀ hq₀')  rw [← mul_div_mul_right _ _ hne.ne']  have eq₁ : p⁻¹.toReal * (q⁻¹.toReal - q₀⁻¹.toReal) *      (p.toReal * q.toReal * p₀.toReal * q₀.toReal) =      p₀.toReal * (p⁻¹.toReal * p.toReal) * ((q⁻¹.toReal * q.toReal) * q₀.toReal -      (q₀⁻¹.toReal * q₀.toReal) * q.toReal) := by ring  have eq₂ : q⁻¹.toReal * (p⁻¹.toReal - p₀⁻¹.toReal) *      (p.toReal * q.toReal * p₀.toReal * q₀.toReal) =      q₀.toReal * (q⁻¹.toReal * q.toReal) * ((p⁻¹.toReal * p.toReal) * p₀.toReal -      (p₀⁻¹.toReal * p₀.toReal) * p.toReal) := by ring  rw [eq₁, eq₂, ← @toReal_mul q⁻¹ q, ← @toReal_mul p⁻¹ p, ← @toReal_mul p₀⁻¹ p₀,      ← @toReal_mul q₀⁻¹ q₀]  all_goals try assumption  -- TODO: why can below goals not be discharged?  repeat rw [ENNReal.inv_mul_cancel] <;> try positivity  all_goals simp <;> try assumption  · apply interp_exp_ne_top hq₀q₁ ht hq  · apply interp_exp_ne_top hp₀p₁ ht hp