lean_workbook_plus_32538
ProvedLet $a, b, c, d$ be positive numbers such that $a^2+b^2=40, c^2+d^2=10, ac-bd=12$ . Find the value of $ad+bc$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32538 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (hab : a^2 + b^2 = 40) (hcd : c^2 + d^2 = 10) (h : a * c - b * d = 12) : a * d + b * c = 16 := by sorry
Source