import Mathlib

/- Proof of the Cauchy-Scwarz inequality. -/

open Set Classical Real

--theorem ineq_lemma0 {α : Type*} [LinearOrderedCommRing α] {a b c : α}
--    (hb : 0 <= b) (habc : a + b = c) : a <= c := by
--  sorry
--
--theorem ineq_lemma1 {α : Type*} [LinearOrderedCommRing α] {a b c : α}
--    (hb : 0 ≤ b) (habc : a + b = c) : a ≤ c := by
--  linarith
--
--theorem ineq_lemma2 {α : Type*} [LinearOrderedCommRing α] {a b c : α}
--    (hb : 0 ≤ b) (habc : a + b = c) : a ≤ c := by
--  calc
--    _ ≤ _ := le_add_of_nonneg_right hb
--    _ = _ := habc

theorem CauchySchwarz2
    (a1 a2 : Real) (b1 b2 : ℝ) :
--theorem CauchySchwarz2 {α : Type*} [LinearOrderedCommRing α]
--    (a1 a2 : α) (b1 b2 : α) :
---theorem CauchySchwarz2 {α : Type*} [LinearOrderedCommRing α] :
---    ∀ (a1 a2 : α), ∀ (b1 b2 : α),
      (a1 * b1 + a2 * b2) ^ 2 ≤ (a1 ^ 2 + a2 ^ 2) * (b1 ^ 2 + b2 ^ 2) := by
---  intro a1 a2 b1 b2
  have h : (a1 * b1 + a2 * b2) ^ 2 + (a1 * b2 - a2 * b1) ^ 2 =
      (a1 ^ 2 + a2 ^ 2) * (b1 ^ 2 + b2 ^ 2) := by
    ring -- or
    --linarith
  have hnneg : 0 ≤ (a1 * b2 - a2 * b1) ^ 2 := by
    -- Moogle: square is nonnegative
    exact sq_nonneg _
    --exact?
  sorry -- or
  --exact ineq_lemma0 (by assumption) h -- or
  ---exact ineq_lemma1 (by assumption) h -- or
  ----exact ineq_lemma2 (by assumption) h -- or
  -----calc
  -----  -- Moogle: le of add (right) nonneg
  -----  _ ≤ _ := le_add_of_nonneg_right hnneg
  -----  _ = _ := h

-- check if a theorem relies on `sorry`
#print axioms ineq_lemma0
#print axioms ineq_lemma1
#print axioms ineq_lemma2
#print axioms CauchySchwarz2

-- fails for Nat, because it is not a ring
example : (10 * 2 + 3 * 7) ^ 2 ≤ (10 ^2 + 3 ^ 2) * (2 ^ 2 + 7 ^ 2) := by
  apply CauchySchwarz2

#synth LinearOrderedCommRing Nat
#synth LinearOrderedCommRing ℕ

-- works for Real
--#synth LinearOrderedCommRing Real
--#synth LinearOrderedCommRing ℝ

example : ((10 * 2 + 3 * 7) ^ 2 : Real) ≤ (10 ^ 2 + 3 ^ 2) * (2 ^ 2 + 7 ^ 2) := by
  apply CauchySchwarz2

-- works for Integer
#synth LinearOrderedCommRing Int
#synth LinearOrderedCommRing ℤ

example : ((10 * 2 + 3 * 7) ^ 2 : Int) ≤ (10 ^ 2 + 3 ^ 2) * (2 ^ 2 + 7 ^ 2) := by
  apply CauchySchwarz2