F₄ sq mul eq

lemma f₄_sq_mul_eq (z : ℍ) (hg_z : theta_g z = 0) :    f₄ z ^ 2 * (3 * H_sum_sq z) = (2 * H₂ z + H₄ z) ^ 2 * theta_h z := by  unfold H_sum_sq  -- Define A = 2H₂ + H₄, B = H₂ + 2H₄  set A := 2 * H₂ z + H₄ z with hA  set B := H₂ z + 2 * H₄ z with hB  -- From theta_g = 0: A * f₂ + B * f₄ = 0  have h_Af₂_eq : A * f₂ z + B * f₄ z = 0 := by    simp only [theta_g, hA, hB, smul_eq_mul, Pi.smul_apply, Pi.mul_apply, Pi.add_apply] at hg_z ⊢    linear_combination hg_z  -- Af₂ = -Bf₄  have hAf₂ : A * f₂ z = -(B * f₄ z) := by linear_combination h_Af₂_eq  -- A²f₂² = B²f₄²  have h1 : A ^ 2 * f₂ z ^ 2 = B ^ 2 * f₄ z ^ 2 := by    have h_sq : (A * f₂ z) ^ 2 = (B * f₄ z) ^ 2 := by rw [hAf₂]; ring    calc A ^ 2 * f₂ z ^ 2 = (A * f₂ z) ^ 2 := by ring      _ = (B * f₄ z) ^ 2 := h_sq      _ = B ^ 2 * f₄ z ^ 2 := by ring  -- A²f₂f₄ = -ABf₄²  have h2 : A ^ 2 * (f₂ z * f₄ z) = -(A * B * f₄ z ^ 2) := by    calc A ^ 2 * (f₂ z * f₄ z) = (A * f₂ z) * (A * f₄ z) := by ring      _ = (-(B * f₄ z)) * (A * f₄ z) := by rw [hAf₂]      _ = -(A * B * f₄ z ^ 2) := by ring  -- A² - AB + B² = 3(H₂² + H₂H₄ + H₄²)  have h_sum : A ^ 2 - A * B + B ^ 2 = 3 * (H₂ z ^ 2 + H₂ z * H₄ z + H₄ z ^ 2) := by    simp only [hA, hB]; ring  -- Now compute A²θₕ  unfold theta_h  calc f₄ z ^ 2 * (3 * (H₂ z ^ 2 + H₂ z * H₄ z + H₄ z ^ 2))      = f₄ z ^ 2 * (A ^ 2 - A * B + B ^ 2) := by rw [h_sum]    _ = B ^ 2 * f₄ z ^ 2 + (-(A * B * f₄ z ^ 2)) + A ^ 2 * f₄ z ^ 2 := by ring    _ = A ^ 2 * f₂ z ^ 2 + A ^ 2 * (f₂ z * f₄ z) + A ^ 2 * f₄ z ^ 2 := by rw [h1, h2]    _ = A ^ 2 * (f₂ z ^ 2 + f₂ z * f₄ z + f₄ z ^ 2) := by ring