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 / (p₀.toReal - p.toReal) := by  rw [ζ_equality₁ ht, ← preservation_interpolation ht hp₀ hp₁ hp,    ← preservation_interpolation ht hq₀ hq₁ hq, hq₀']  simp only [inv_top, toReal_zero, sub_zero]  have obs : 0 < p₀.toReal * p.toReal * q.toReal :=    mul_pos (mul_pos (toReal_pos hp₀.ne' hp₀') (interp_exp_toReal_pos ht hp₀ hp₁ hp₀p₁ hp))      (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq)  rw [← mul_div_mul_right _ _ obs.ne']  congr  · calc    _ = (p.toReal⁻¹ * p.toReal) * (q.toReal⁻¹ * q.toReal) * p₀.toReal := by      rw [toReal_inv, toReal_inv]      ring    _ = _ := by      rw [inv_mul_cancel₀, inv_mul_cancel₀, one_mul, one_mul]      · exact (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq).ne'      · exact (interp_exp_toReal_pos ht hp₀ hp₁ hp₀p₁ hp).ne'  · calc    _ = (q.toReal⁻¹ * q.toReal) * (p.toReal⁻¹ * p.toReal * p₀.toReal - p₀.toReal⁻¹ *        p₀.toReal * p.toReal) := by      rw [toReal_inv, toReal_inv, toReal_inv]      ring    _ = _ := by      repeat rw [inv_mul_cancel₀, one_mul]      · exact (toReal_pos hp₀.ne' hp₀').ne'      · exact (interp_exp_toReal_pos ht hp₀ hp₁ hp₀p₁ hp).ne'      · exact (interp_exp_toReal_pos ht hq₀ hq₁ hq₀q₁ hq).ne'