Hlawka_inequality.lean

--Author: Cristian Calin

--In this file we shall prove Hlawka's Inequality, which states that, for a real vector space, if x, y, z ∈ V,
--|x+y+z|+|x|+|y|+|z| ≥ |x+y| + |y+z| + |x+z|. The proof was taken from the paper
--"Generalizations of the Hlawka's inequality" by Honda et al.

import algebra 
import tactic
import data.real.basic
import algebra.quadratic_discriminant

structure inner_product (V : Type) [add_comm_group V] [vector_space ℝ V] := 
(inner : V → V → ℝ)
(inner_add_left: ∀ x y z : V, inner (x+y) z= inner x z + inner y z)
(inner_smul_left: ∀ x y : V, ∀ a : ℝ, inner(a • x) y=a * inner x y)
(inner_add_right: ∀ x y z : V, inner x (y+z) = inner x y + inner x z)
(inner_smul_right: ∀ x y: V, ∀ a : ℝ, inner x (a • y)=a * inner x y)
(inner_positive: ∀ x : V, inner x x ≥ 0)
(inner_zero_iff_zero: ∀ x : V, inner x x=0 ↔ x = (0:V))
(inner_comm: ∀ x y : V, inner x y = inner y x)

variables {V: Type} [add_comm_group V] [vector_space ℝ V] 

variable {f: inner_product V}

instance : has_coe_to_fun (inner_product V) :=
⟨_, λ f, f.inner⟩

@[simp] lemma coe_fn_mk (f : V → V → ℝ) (h₁ h₂ h₃ h₄ h₅ h₆ h₇ ) :
  (inner_product.mk f h₁ h₂ h₃ h₄ h₅ h₆ h₇: V → V → ℝ) = f :=
rfl

@[simp] theorem coe_to_inner: ∀ x y : V, f x y = f.inner x y:=
begin
intros x y,
refl,
end

lemma three_add_comm (a b c : V): c + a + b = a + b + c:=
begin
rw add_assoc c a b,
rw add_comm (a+b) c,
end

lemma three_add_comm' (x y z : V): x + y + z = x + z + y:=
begin
rw add_assoc x y z,
rw add_assoc x z y,
rw add_comm y z,
end

lemma smul_right': ∀ x : V, f x ((0 : ℝ) • x) = (0 : ℝ) * f x x:=
begin
intro x,
rw (coe_to_inner x x),
rw (coe_to_inner x ((0 : ℝ) • x)),
apply f.inner_smul_right x x 0,
end

lemma smul_left': ∀ x : V, f ((0 : ℝ) • x) x = (0 : ℝ) * f x x:=
begin
intro x,
rw (coe_to_inner x x),
rw (coe_to_inner ((0 : ℝ) • x) x),
apply f.inner_smul_left x x 0,
end

lemma inner_product_zero_right: ∀ x : V, f x (0:V) = (0 : ℝ):=
begin
intro x,
rw ((zero_smul ℝ x).symm) at *,
calc f x (0 • x) = 0 * f x x: smul_right' x
...=0: by ring,
end

lemma inner_product_zero_left: ∀ x : V, f (0:V) x = (0 : ℝ):=
begin
intro x,
rw ((zero_smul ℝ x).symm) at *,
calc f (0 • x) x = 0 * f x x: smul_left' x
...=0: by ring,
end

theorem neg_one_smul' (x : V) : (-1 : ℝ) • x = -x := by simp

lemma three_term_add_assoc (a b c d : V): a + (b + c + d) = a + b + c + d:=
begin
rw (add_assoc b c d),
rw ← add_assoc a b (c+d),
exact (add_assoc (a + b) c d).symm,
end

lemma special_three_term_add_assoc (a b c : V): -a + (a + b + c) = b + c:=
begin
rw (three_term_add_assoc (-a) a b c),
rw (neg_add_self a),
rw zero_add,
end

lemma sum_pos (α β γ : ℝ) (hα: 0 ≤ α) (hβ: 0 ≤ β) (hγ: 0 ≤ γ) : 0 ≤ α + β + γ:=
begin
linarith,
end


lemma sqrt_of_inner_exists: ∀ x : V, ∃ a : ℝ, 0 ≤ a ∧ a * a = f x x:=
begin
intro x,
exact real.sqrt_exists (f.inner_positive x),
end 

local notation `|` x `|` := real.sqrt (f x x)

lemma norm_square_eq_inner_product: ∀ x : V, |x|*|x| = f x x:=
begin
intro x,
exact real.mul_self_sqrt (f.inner_positive x),
end 

lemma norm_special_three_term_add_assoc (a b c : V): |(((-1):ℝ) • a) + (a + b + c)| = |b + c|:=
begin
rw neg_one_smul',
rw special_three_term_add_assoc a b c,
end

lemma Cauchy_Schwartz: ∀ x y : V, abs(f x y) ≤ |x|*|y|:=
begin
intros x y,
have fact': ∀ a : ℝ, f (x + a • y) (x + a • y) = f x x + 2 * a * f x y + a^2 * f y y,
{    
    intro a,
    calc f (x + a • y) (x + a • y) = f x (x + a • y) + f (a • y) (x + a • y): by exact f.inner_add_left x (a • y) (x + a • y)
    ...= f x (x + a • y) + (a * f y (x + a • y)): congr_arg (has_add.add (f x (x + a • y))) (f.inner_smul_left y (x+ a•y) a)
    ...= (f x x + f x (a • y)) + (a * f y (x + a • y)): congr_fun (congr_arg has_add.add (f.inner_add_right x x (a • y))) (a * f y (x + a • y))
    ...= (f x x + (a * f x y)) + (a * f y (x + a • y)): congr (congr_arg has_add.add (congr_arg (has_add.add (f x x)) (f.inner_smul_right x y a))) rfl
    ...= (f x x + (a * f x y)) + (a * (f y x + f y (a • y))): congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (f.inner_add_right y x (a • y)))
    ...= (f x x + (a * f x y)) + (a * (f y x + (a * f y y))): congr rfl (congr_arg (has_mul.mul a) (congr_arg (has_add.add (f y x)) (f.inner_smul_right y y a)))
    ...= f x x + a * f x y + a * f y x + a^2 * f y y: by ring
    ...= f x x + a * f x y + a * f x y + a^2 * f y y: congr_arg2 has_add.add (congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (eq.symm (f.inner_comm x y)))) rfl
    ...= f x x + 2 * a * f x y + a ^ 2 * f y y : by ring,
},
have factfinal: ∀ a : ℝ, 0 ≤ f x x + 2 * a * f x y + a ^ 2 * f y y,
{
    intro a,
    calc 0 ≤ f (x + a • y) (x + a • y): f.inner_positive (x + a • y)
    ...= f x x + 2 * a * f x y + a ^ 2 * f y y : fact' a,
},

have obv: ∀ a : ℝ, a * a = a ^ 2,
{
    intro a,
    ring,
},

have factfinal': ∀ a : ℝ, 0 ≤ f x x + 2 * a * f x y + a * a * f y y,
{
    intro a,
    calc 0 ≤ f x x + 2 * a * f x y + a ^ 2 * f y y : factfinal a
    ...= f x x + 2 * a * f x y + a * a * f y y: congr rfl (congr_fun (congr_arg has_mul.mul (eq.symm (obv a))) (f y y)),
},

have  factfinal'': ∀ a : ℝ, 0 ≤ f y y * a * a + 2 * f x y * a + f x x,
{
    intro a,
    calc 0 ≤ f x x + 2 * a * f x y + a * a * f y y: factfinal' a
    ...= f y y * a * a + 2 * f x y * a + f x x : by ring,
},

clear fact' factfinal obv factfinal',

have discrim_def: ∀ a b c : ℝ, discrim a b c = b ^ 2 - 4 * a * c,
{
    intros a b c,
    rw discrim,
},
have fact: (2 * f x y) ^ 2 - 4 * f y y * f x x ≤ 0,
{
    calc (2 * f x y) ^ 2 - 4 * f y y * f x x = discrim (f y y) (2 * f x y) (f x x): eq.symm (discrim_def (f y y) (2 * f x y) (f x x))
    ...≤ 0: by exact (discriminant_le_zero factfinal''),
},
ring at fact,
have fact': 4 * ((f x y)^2) ≤ 4 * (f x x * f y y),
{
    calc 4 * ((f x y)^2) = 4 * (f x y)^2: by ring
    ...≤ 4 * f x x * f y y: by exact sub_nonpos.mp fact
    ...= 4 * (f x x * f y y): by ring,
},
have h: real.sqrt(f x x * f y y)=real.sqrt(f x x) * real.sqrt (f y y),
{
    exact real.sqrt_mul (f.inner_positive x) (f y y),
},
have obs: real.sqrt((f x y)^2) ≤ real.sqrt(f x x * f y y),
{
    have obs: (0:ℝ) < 4, {linarith,},
    exact real.sqrt_le_sqrt (le_of_mul_le_mul_left fact' obs),
},
rw (f x y).sqrt_sqr_eq_abs at obs,
rw h  at obs,
exact obs,
end 

lemma triangle_inequality: ∀ x y : V, |x + y| ≤ |x| + |y|:=
begin
intros x y,
have fact: |x+y|*|x+y| = f x x + f x y + f y x + f y y,
{
   calc |x+y|*|x+y|=f (x+y) (x+y): norm_square_eq_inner_product (x + y)
   ...= f x (x+y) + f y (x+y): by exact f.inner_add_left x y (x+y)
   ...= (f x x + f x y) + f y (x+y) : congr_fun (congr_arg has_add.add (f.inner_add_right x x y)) (f y (x + y))
   ...= (f x x + f x y) + (f y x + f y y): congr_arg (has_add.add (f x x + f x y)) (f.inner_add_right y x y)
   ...= f x x + f x y + f y x + f y y: by ring,
},
have fact2: (|x|+|y|)*(|x|+|y|) = f x x + f y y + 2*|x|*|y|,
{
   calc (|x|+|y|)*(|x|+|y|) = |x|*|x|+2*|x|*|y|+|y|*|y|: by ring
   ...= f x x + 2 * |x| * |y| + |y|*|y|: congr_arg2 has_add.add (congr_fun (congr_arg has_add.add (norm_square_eq_inner_product x)) (2 * real.sqrt (f x x) * real.sqrt (f y y))) rfl
   ...= f x x + 2 * |x| * |y| + f y y: congr_arg (has_add.add (f x x + 2 * real.sqrt (f x x) * real.sqrt (f y y))) (norm_square_eq_inner_product y)
   ...= f x x + f y y + 2 * |x| * |y|: by ring,
},
have fact0: |x+y|*|x+y|= f x x + 2 * f x y + f y y,
{
    calc |x+y|*|x+y|= f x x + f x y + f y x + f y y: fact
    ...= f x x + f x y + f x y + f y y : congr (congr_arg has_add.add (congr_arg (has_add.add (f x x + f x y)) (eq.symm (f.inner_comm x y)))) rfl
    ...= f x x + 2 * f x y + f y y: by ring,
},
clear fact,
have obs: 2 * f x y ≤ 2 * |x| * |y|,
{
   have obs': f x y ≤ |x| * |y|,
   {
      calc f x y ≤ abs (f x y): le_abs_self (f x y)
      ...≤ |x| * |y|: by exact Cauchy_Schwartz x y,
   },
   linarith,
},
have observation: |x+y|*|x+y| ≤ (|x|+|y|)*(|x|+|y|),
{
    linarith,
},
clear fact2 fact0 obs,
rw (norm_square_eq_inner_product (x+y)) at observation,
have h1: 0 ≤ |x| + |y|,
{
   calc 0 ≤ |x|: by exact ((f x x).sqrt_nonneg)
   ...= |x| + 0: by ring
   ...≤ |x| + |y|: add_le_add_left ((f y y).sqrt_nonneg) (real.sqrt (f x x)),
},
have h2: |x|+|y|=real.sqrt((|x|+|y|)*(|x|+|y|)),
{
    exact (real.sqrt_mul_self h1).symm,
},
have h3: (|x|+|y|)*(|x|+|y|)=(|x|+|y|)^2,
{
    ring,
},
rw h3 at observation,
rw h3 at h2,
clear h3 h1,
calc real.sqrt(f (x+y) (x+y)) ≤ real.sqrt(((real.sqrt (f x x)) + real.sqrt (f y y))^2): by exact real.sqrt_le_sqrt observation
...=|x|+|y|: eq.symm h2,
end 

lemma norm_special_sum: ∀ x y z : V, (|x+y+z|*|x+y+z|+|x|*|x+y+z|+|y|*|x+y+z|+|z|*|x+y+z|+|x+y+z|*|x|+|x|*|x|+|y|*|x|+|z|*|x|+|x+y+z|*|y|+|x|*|y|+|y|*|y|+|z|*|y|+|x+y+z|*|z|+|x|*|z|+|y|*|z|+|z|*|z|)-(|x+y|*|x+y+z|+|x+z|*|x+y+z|+|y+z|*|x+y+z|+|x+y|*|x|+|x+z|*|x|+|y+z|*|x|+|x+y|*|y|+|y+z|*|y|+|x+z|*|y|+|x+y|*|z|+|x+z|*|z|+|y+z|*|z|)=
(f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z + |x|*|x+y+z|+|y|*|x+y+z|+|z|*|x+y+z|+|x+y+z|*|x| + f x x + |y|*|x| + |z|*|x| + |x+y+z|*|y| + |x|*|y| + f y y + |z|*|y| + |x+y+z|*|z| + |x|*|z| + |y|*|z| + f z z) - (|x+y|*|x+y+z| + |x+z|*|x+y+z| + |y+z|*|x+y+z| + |x+y|*|x| + |x+z|*|x| + |y+z|*|x| + |x+y|*|y| + |y+z|*|y| + |x+z|*|y| + |x+y|*|z| + |x+z|*|z| + |y+z|*|z|):=
begin
intros x y z,
rw (norm_square_eq_inner_product (x + y + z)),
have hsum31: ∀ a b c d : V, f (a+b+c) d = f a d + f b d + f c d,
{
    intros a b c d,
    calc f (a+b+c) d = f (a+(b+c)) d: congr (congr_arg ⇑f (add_assoc a b c)) rfl
    ...= f a d + f (b+c) d: by exact f.inner_add_left a (b+c) d
    ...= f a d + (f b d + f c d): congr_arg (has_add.add (f a d)) (f.inner_add_left b c d)
    ...= f a d + f b d + f c d : by ring,
},

have hsum32: ∀ a b c d : V, f a (b+c+d) = f a b + f a c + f a d,
{
    intros a b c d,
    calc f a (b+c+d) = f a ((b+c)+d): rfl
    ...= f a (b+c) + f a d: by exact f.inner_add_right a (b+c) d
    ...= (f a b + f a c) + f a d: congr_fun (congr_arg has_add.add (f.inner_add_right a b c)) (f a d)
    ...= f a b + f a c + f a d: by ring,
},
have hxyz: f (x+y+z) (x+y+z) = f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z,
{
   calc f (x+y+z) (x+y+z) = f (x+y+z) x + f (x+y+z) y + f (x+y+z) z : by exact hsum32 (x+y+z) x y z
   ...= (f x x + f y x + f z x) + f (x+y+z) y + f (x+y+z) z : congr_arg2 has_add.add (congr_fun (congr_arg has_add.add (hsum31 x y z x)) (f (x + y + z) y)) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + f (x+y+z) z: congr (congr_arg has_add.add (congr_arg (has_add.add (f x x + f y x + f z x)) (hsum31 x y z y))) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + (f x z + f y z + f z z): congr_arg (has_add.add (f x x + f y x + f z x + (f x y + f y y + f z y))) (hsum31 x y z z)
   ...= f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z: by ring,
},
have hxy: f (x+y) (x+y) = f x x + f x y + f y x + f y y,
{
    calc f (x+y) (x+y) = f x (x+y) + f y (x+y): by exact f.inner_add_left x y (x+y)
    ...= (f x x + f x y) + f y (x+y): congr_fun (congr_arg has_add.add (f.inner_add_right x x y)) (f y (x + y))
    ...= (f x x + f x y) + (f y x + f y y): congr_arg (has_add.add (f x x + f x y)) (f.inner_add_right y x y)
    ...= f x x + f x y + f y x + f y y: by ring,
},
have hyz: f (y+z) (y+z) = f y y + f y z + f z y + f z z,
{
    calc f (y+z) (y+z) = f y (y+z) + f z (y+z) : by exact f.inner_add_left y z (y+z)
    ...= (f y y + f y z) + f z (y+z): congr_fun (congr_arg has_add.add (f.inner_add_right y y z)) (f z (y + z))
    ...= (f y y + f y z) + (f z y + f z z): congr_arg (has_add.add (f y y + f y z)) (f.inner_add_right z y z)
    ...= f y y + f y z + f z y + f z z: by ring,
},
have hxz: f (x+z) (x+z) = f x x + f x z + f z x + f z z,
{
    calc f (x+z) (x+z) = f x (x+z) + f z (x+z): by exact f.inner_add_left x z (x+z)
    ...= (f x x + f x z) + f z (x+z): congr_fun (congr_arg has_add.add (f.inner_add_right x x z)) (f z (x + z))
    ...= (f x x + f x z) + (f z x + f z z): congr_arg (has_add.add (f x x + f x z)) (f.inner_add_right z x z)
    ...= f x x + f x z + f z x + f z z: by ring,
},
let a:=|x+y+z|,
have ha: |x+y+z| = a,
{
    exact rfl,
},
rw ha at *,
rw hxyz at *,
have h': ∀ x : V, |x|*|x|= f x x,
{
    intro x,
    exact norm_square_eq_inner_product x,
},
rw (h' x) at *,
rw (h' y) at *,
rw (h' z) at *,
end

lemma norm_same_negative: ∀ x : V, |x|=|((-1):ℝ) • x| :=
begin
have fact': ∀ a : ℝ, ∀ x y : V, f (x + a • y) (x + a • y) = f x x + 2 * a * f x y + a^2 * f y y,
{    
    intros a x y,
    calc f (x + a • y) (x + a • y) = f x (x + a • y) + f (a • y) (x + a • y): by exact f.inner_add_left x (a • y) (x + a • y)
    ...= f x (x + a • y) + (a * f y (x + a • y)): congr_arg (has_add.add (f x (x + a • y))) (f.inner_smul_left y (x+a•y) a)
    ...= (f x x + f x (a • y)) + (a * f y (x + a • y)): congr_fun (congr_arg has_add.add (f.inner_add_right x x (a•y))) (a * f y (x + a • y))
    ...= (f x x + (a * f x y)) + (a * f y (x + a • y)): congr (congr_arg has_add.add (congr_arg (has_add.add (f x x)) ( f.inner_smul_right x y a))) rfl
    ...= (f x x + (a * f x y)) + (a * (f y x + f y (a • y))): congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (f.inner_add_right y x (a • y)))
    ...= (f x x + (a * f x y)) + (a * (f y x + (a * f y y))): congr rfl (congr_arg (has_mul.mul a) (congr_arg (has_add.add (f y x)) (f.inner_smul_right y y a)))
    ...= f x x + a * f x y + a * f y x + a^2 * f y y: by ring
    ...= f x x + a * f x y + a * f x y + a^2 * f y y: congr_arg2 has_add.add (congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (f.inner_comm y x))) rfl
    ...= f x x + 2 * a * f x y + a ^ 2 * f y y : by ring,
},
intro x,
specialize fact' ((-1):ℝ) (0:V) x,
rw zero_add at *, 
rw (inner_product_zero_right (0:V)) at fact',
rw (inner_product_zero_left x) at fact',
ring at fact',
rw eq.symm (fact'),
end

section Hlawka

lemma Hlawka_equality (x y z : V):
f x x + f y y + f z z + f (x+y+z) (x+y+z) = f (x+y) (x+y) + f (x+z) (x+z) + f (y+z) (y+z) :=
begin
have hxy: f (x+y) (x+y) = f x x + f x y + f y x + f y y,
{
    calc f (x+y) (x+y) = f x (x+y) + f y (x+y): by exact f.inner_add_left x y (x+y)
    ...= (f x x + f x y) + f y (x+y): congr_fun (congr_arg has_add.add (f.inner_add_right x x y)) (f y (x + y))
    ...= (f x x + f x y) + (f y x + f y y): congr_arg (has_add.add (f x x + f x y)) (f.inner_add_right y x y)
    ...= f x x + f x y + f y x + f y y: by ring,
},
have hyz: f (y+z) (y+z) = f y y + f y z + f z y + f z z,
{
    calc f (y+z) (y+z) = f y (y+z) + f z (y+z) : by exact f.inner_add_left y z (y+z)
    ...= (f y y + f y z) + f z (y+z): congr_fun (congr_arg has_add.add (f.inner_add_right y y z)) (f z (y + z))
    ...= (f y y + f y z) + (f z y + f z z): congr_arg (has_add.add (f y y + f y z)) (f.inner_add_right z y z)
    ...= f y y + f y z + f z y + f z z: by ring,
},
have hxz: f (x+z) (x+z) = f x x + f x z + f z x + f z z,
{
    calc f (x+z) (x+z) = f x (x+z) + f z (x+z): by exact f.inner_add_left x z (x+z)
    ...= (f x x + f x z) + f z (x+z): congr_fun (congr_arg has_add.add (f.inner_add_right x x z)) (f z (x + z))
    ...= (f x x + f x z) + (f z x + f z z): congr_arg (has_add.add (f x x + f x z)) (f.inner_add_right z x z)
    ...= f x x + f x z + f z x + f z z: by ring,
},
rw [hxy, hyz, hxz],
have hsum31: ∀ a b c d : V, f (a+b+c) d = f a d + f b d + f c d,
{
    intros a b c d,
    calc f (a+b+c) d = f (a+(b+c)) d: congr (congr_arg ⇑f (add_assoc a b c)) rfl
    ...= f a d + f (b+c) d: by exact f.inner_add_left a (b+c) d
    ...= f a d + (f b d + f c d): congr_arg (has_add.add (f a d)) (f.inner_add_left b c d)
    ...= f a d + f b d + f c d : by ring,
},

have hsum32: ∀ a b c d : V, f a (b+c+d) = f a b + f a c + f a d,
{
    intros a b c d,
    calc f a (b+c+d) = f a ((b+c)+d): rfl
    ...= f a (b+c) + f a d: by exact f.inner_add_right a (b+c) d
    ...= (f a b + f a c) + f a d: congr_fun (congr_arg has_add.add (f.inner_add_right a b c)) (f a d)
    ...= f a b + f a c + f a d: by ring,
},
have hxyz: f (x+y+z) (x+y+z) = f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z,
{
   calc f (x+y+z) (x+y+z) = f (x+y+z) x + f (x+y+z) y + f (x+y+z) z : by exact hsum32 (x+y+z) x y z
   ...= (f x x + f y x + f z x) + f (x+y+z) y + f (x+y+z) z : congr_arg2 has_add.add (congr_fun (congr_arg has_add.add (hsum31 x y z x)) (f (x + y + z) y)) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + f (x+y+z) z: congr (congr_arg has_add.add (congr_arg (has_add.add (f x x + f y x + f z x)) (hsum31 x y z y))) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + (f x z + f y z + f z z): congr_arg (has_add.add (f x x + f y x + f z x + (f x y + f y y + f z y))) (hsum31 x y z z)
   ...= f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z: by ring,
},
rw hxyz,
ring,
end

open classical
local attribute [instance] prop_decidable

theorem Hlawka_inequality : ∀ x y z : V, |x + y| + |x + z| + |y + z| ≤ |x| + |y| + |z| + |x + y + z|:=
begin
intros x y z,
have obs: x = (0:V) ∨ x ≠ (0:V),
{
  exact classical.em (x = 0),  
},
by_cases obs': x = (0:V),
{
  clear obs,
  rw obs' at *,
  rw zero_add at *,
  rw zero_add at *,
  have obs: f 0 0 = 0,
  {
      exact inner_product_zero_right 0,
  },
  rw obs at *,
  rw (real.sqrt_zero) at *,
  ring,
},
{have obs: x ≠ 0,
    {
        exact obs',
    },
    clear obs,
    have hx: 0 < |x|,
    {
        have obs: 0 ≤ |x|,
        {
            exact (f x x).sqrt_nonneg,
        },
        have fact': f x x ≠ 0 ↔ x ≠ (0 : V),
        {
            exact not_congr (f.inner_zero_iff_zero x),
        },
        have fact'': f x x ≠ 0,
        {
            tauto,
        },
        have obv: 0 < f x x,
        {
            exact lt_of_le_of_ne (f.inner_positive x) (ne.symm fact''),
        },
        exact real.sqrt_pos.mpr obv,
    },
    have hsum: 0 < |x|+|y|+|z|+|x+y+z|,
    {
        linarith[hx, (f y y).sqrt_nonneg, (f z z).sqrt_nonneg, (f (x+y+z)(x+y+z)).sqrt_nonneg],
    },
    have obs: ((|x+y+z|+|x|+|y|+|z|)-(|x+y|+|x+z|+|y+z|))*(|x+y+z|+|x|+|y|+|z|)=((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|)+((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|)+((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|),
    {
        have h1: ((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|)=(|x|*|z|+|y|*|z|+|x|*|x+y+z|+|y|*|x+y+z|+|x+y|*|x+y|) - (|x+y|*|z|+|x+y|*|x+y+z|+|x|*|x+y|+|y|*|x+y|),
        {
            ring,
        },
        have h2: ((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|)=(|x|*|y|+|z|*|y|+|x|*|x+y+z|+|z|*|x+y+z|+|x+z|*|x+z|) - (|x+z|*|y|+|x+z|*|x+y+z|+|x|*|x+z|+|z|*|x+z|),
        {
            ring,
        },
        have h3: ((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|)=(|y|*|x|+|z|*|x|+|y|*|x+y+z|+|z|*|x+y+z|+|y+z|*|y+z|) - (|y+z|*|x|+|y+z|*|x+y+z|+|y|*|y+z|+|z|*|y+z|),
        {
            ring,
        },
        have h4: ((|x+y+z|+|x|+|y|+|z|)-(|x+y|+|x+z|+|y+z|))*(|x+y+z|+|x|+|y|+|z|)=(|x+y+z|*|x+y+z|+|x|*|x+y+z|+|y|*|x+y+z|+|z|*|x+y+z|+|x+y+z|*|x|+|x|*|x|+|y|*|x|+|z|*|x|+|x+y+z|*|y|+|x|*|y|+|y|*|y|+|z|*|y|+|x+y+z|*|z|+|x|*|z|+|y|*|z|+|z|*|z|)-(|x+y|*|x+y+z|+|x+z|*|x+y+z|+|y+z|*|x+y+z|+|x+y|*|x|+|x+z|*|x|+|y+z|*|x|+|x+y|*|y|+|y+z|*|y|+|x+z|*|y|+|x+y|*|z|+|x+z|*|z|+|y+z|*|z|),
        {
            ring,
        },
        rw (norm_special_sum x y z) at h4,
have hxy: f (x+y) (x+y) = f x x + f x y + f y x + f y y,
{
    calc f (x+y) (x+y) = f x (x+y) + f y (x+y): by exact f.inner_add_left x y (x+y)
    ...= (f x x + f x y) + f y (x+y): congr_fun (congr_arg has_add.add (f.inner_add_right x x y)) (f y (x + y))
    ...= (f x x + f x y) + (f y x + f y y): congr_arg (has_add.add (f x x + f x y)) (f.inner_add_right y x y)
    ...= f x x + f x y + f y x + f y y: by ring,
},
have hyz: f (y+z) (y+z) = f y y + f y z + f z y + f z z,
{
    calc f (y+z) (y+z) = f y (y+z) + f z (y+z) : by exact f.inner_add_left y z (y+z)
    ...= (f y y + f y z) + f z (y+z): congr_fun (congr_arg has_add.add (f.inner_add_right y y z)) (f z (y + z))
    ...= (f y y + f y z) + (f z y + f z z): congr_arg (has_add.add (f y y + f y z)) (f.inner_add_right z y z)
    ...= f y y + f y z + f z y + f z z: by ring,
},
have hxz: f (x+z) (x+z) = f x x + f x z + f z x + f z z,
{
    calc f (x+z) (x+z) = f x (x+z) + f z (x+z): by exact f.inner_add_left x z (x+z)
    ...= (f x x + f x z) + f z (x+z): congr_fun (congr_arg has_add.add (f.inner_add_right x x z)) (f z (x + z))
    ...= (f x x + f x z) + (f z x + f z z): congr_arg (has_add.add (f x x + f x z)) (f.inner_add_right z x z)
    ...= f x x + f x z + f z x + f z z: by ring,
},
have hsum31: ∀ a b c d : V, f (a+b+c) d = f a d + f b d + f c d,
{
    intros a b c d,
    calc f (a+b+c) d = f (a+(b+c)) d: congr (congr_arg ⇑f (add_assoc a b c)) rfl
    ...= f a d + f (b+c) d: by exact f.inner_add_left a (b+c) d
    ...= f a d + (f b d + f c d): congr_arg (has_add.add (f a d)) (f.inner_add_left b c d)
    ...= f a d + f b d + f c d : by ring,
},

have hsum32: ∀ a b c d : V, f a (b+c+d) = f a b + f a c + f a d,
{
    intros a b c d,
    calc f a (b+c+d) = f a ((b+c)+d): rfl
    ...= f a (b+c) + f a d: by exact f.inner_add_right a (b+c) d
    ...= (f a b + f a c) + f a d: congr_fun (congr_arg has_add.add (f.inner_add_right a b c)) (f a d)
    ...= f a b + f a c + f a d: by ring,
},
have hxyz: f (x+y+z) (x+y+z) = f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z,
{
   calc f (x+y+z) (x+y+z) = f (x+y+z) x + f (x+y+z) y + f (x+y+z) z : by exact hsum32 (x+y+z) x y z
   ...= (f x x + f y x + f z x) + f (x+y+z) y + f (x+y+z) z : congr_arg2 has_add.add (congr_fun (congr_arg has_add.add (hsum31 x y z x)) (f (x + y + z) y)) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + f (x+y+z) z: congr (congr_arg has_add.add (congr_arg (has_add.add (f x x + f y x + f z x)) (hsum31 x y z y))) rfl
   ...= (f x x + f y x + f z x) + (f x y + f y y + f z y) + (f x z + f y z + f z z): congr_arg (has_add.add (f x x + f y x + f z x + (f x y + f y y + f z y))) (hsum31 x y z z)
   ...= f x x + f x y + f x z + f y x + f y y + f y z + f z x + f z y + f z z: by ring,
},
have h1': (|x|*|z|+|y|*|z|+|x|*|x+y+z|+|y|*|x+y+z|+|x+y|*|x+y|) - (|x+y|*|z|+|x+y|*|x+y+z|+|x|*|x+y|+|y|*|x+y|)=(|x|*|z|+|y|*|z|+|x|*|x+y+z|+|y|*|x+y+z|+f (x+y) (x+y))-(|x+y|*|z|+|x+y|*|x+y+z|+|x|*|x+y|+|y|*|x+y|),
{
    exact congr
  (congr_arg has_sub.sub
     (congr_arg
        (has_add.add
           (real.sqrt (f x x) * real.sqrt (f z z) + real.sqrt (f y y) * real.sqrt (f z z) +
                real.sqrt (f x x) * real.sqrt (f (x + y + z) (x + y + z)) +
              real.sqrt (f y y) * real.sqrt (f (x + y + z) (x + y + z))))
        (norm_square_eq_inner_product (x+y))))
  rfl,
},
rw h1' at h1,
clear h1',
have h1'': (|x|*|z|+|y|*|z|+|x|*|x+y+z|+|y|*|x+y+z|+f (x+y) (x+y))-(|x+y|*|z|+|x+y|*|x+y+z|+|x|*|x+y|+|y|*|x+y|) = (|x|*|z|+|y|*|z|+|x|*|x+y+z|+|y|*|x+y+z|+f x x + f x y + f y x + f y y)-(|x+y|*|z|+|x+y|*|x+y+z|+|x|*|x+y|+|y|*|x+y|),
{
    linarith,
},
rw h1'' at h1,
clear h1'',
rw h1,
clear h1,
have h2': (|x|*|y|+|z|*|y|+|x|*|x+y+z|+|z|*|x+y+z|+|x+z|*|x+z|) - (|x+z|*|y|+|x+z|*|x+y+z|+|x|*|x+z|+|z|*|x+z|)=(|x|*|y|+|z|*|y|+|x|*|x+y+z|+|z|*|x+y+z|+f (x+z) (x+z)) - (|x+z|*|y|+|x+z|*|x+y+z|+|x|*|x+z|+|z|*|x+z|),
{
    exact congr
  (congr_arg has_sub.sub
     (congr_arg
        (has_add.add
           (real.sqrt (f x x) * real.sqrt (f y y) + real.sqrt (f z z) * real.sqrt (f y y) +
                real.sqrt (f x x) * real.sqrt (f (x + y + z) (x + y + z)) +
              real.sqrt (f z z) * real.sqrt (f (x + y + z) (x + y + z))))
        (norm_square_eq_inner_product (x+z))))
  rfl,
},
have h2'': (|x|*|y|+|z|*|y|+|x|*|x+y+z|+|z|*|x+y+z|+f (x+z) (x+z)) - (|x+z|*|y|+|x+z|*|x+y+z|+|x|*|x+z|+|z|*|x+z|)=(|x|*|y|+|z|*|y|+|x|*|x+y+z|+|z|*|x+y+z|+f x x + f x z + f z x + f z z) - (|x+z|*|y|+|x+z|*|x+y+z|+|x|*|x+z|+|z|*|x+z|),
{
    linarith,
},
rw h2'' at h2',
rw h2' at h2,
rw h2,
have h3':(|y|*|x|+|z|*|x|+|y|*|x+y+z|+|z|*|x+y+z|+|y+z|*|y+z|) - (|y+z|*|x|+|y+z|*|x+y+z|+|y|*|y+z|+|z|*|y+z|) = (|y|*|x|+|z|*|x|+|y|*|x+y+z|+|z|*|x+y+z|+f (y+z) (y+z)) - (|y+z|*|x|+|y+z|*|x+y+z|+|y|*|y+z|+|z|*|y+z|),
{
    exact congr
  (congr_arg has_sub.sub
     (congr_arg
        (has_add.add
           (real.sqrt (f y y) * real.sqrt (f x x) + real.sqrt (f z z) * real.sqrt (f x x) +
                real.sqrt (f y y) * real.sqrt (f (x + y + z) (x + y + z)) +
              real.sqrt (f z z) * real.sqrt (f (x + y + z) (x + y + z))))
        (norm_square_eq_inner_product (y+z))))
  rfl,
},
have h3'': (|y|*|x|+|z|*|x|+|y|*|x+y+z|+|z|*|x+y+z|+f (y+z) (y+z)) - (|y+z|*|x|+|y+z|*|x+y+z|+|y|*|y+z|+|z|*|y+z|) = (|y|*|x|+|z|*|x|+|y|*|x+y+z|+|z|*|x+y+z|+f y y + f y z + f z y + f z z) - (|y+z|*|x|+|y+z|*|x+y+z|+|y|*|y+z|+|z|*|y+z|),
{
    linarith,
},
rw h3'' at h3',
rw h3' at h3,
rw [h3, h4],
ring,
},
have hab: ∀ a b : V, 0 ≤ (|a|+|b|)-|a+b|,
{
    intros a b,
    exact sub_nonneg.mpr (triangle_inequality a b),
},
have habc: ∀ a b c : V, 0 ≤ (|a| + |a + b + c|) - |b + c|,
{
    intros a b c,
    have obs: (((-1):ℝ) • a) + (a + b + c) = b + c,
    {
        rw (neg_one_smul' a),
        exact special_three_term_add_assoc a b c,
    },
    have fact: |a| + |a + b + c| ≥ |b + c|,
    {
        calc |a| + |a+b+c| = |((-1) : ℝ) • a| + |a + b + c|: by rw norm_same_negative a
        ... ≥ |(((-1):ℝ) • a) + (a + b + c)|: sub_nonneg.mp (hab ((-1) • a) (a + b + c))
        ...= |b + c|: by exact norm_special_three_term_add_assoc a b c,
    },
    exact sub_nonneg.mpr fact,
},
have h1: ∀ a b c : V, 0 ≤ ((|a| + |b|)-|a + b|)*((|c|+|a + b + c|)-|a+b|),
{
    intros a b c,
    rw ← three_add_comm a b c,
    exact mul_nonneg (hab a b) (habc c a b),
},
have h2: 0 ≤ (((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|)),
{
    rw three_add_comm' x y z,
    exact h1 x z y,
},
have h3: 0 ≤ (((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|)),
{
    rw three_add_comm y z x,
    exact h1 y z x,
},
have inequality: 0 ≤ ((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|) + ((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|) + ((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|),
{
exact sum_pos (((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|)) (((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|)) (((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|)) (h1 x y z) h2 h3,
},
have fact': ((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|) + ((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|) + ((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|) = ((|x|+|y|)-|x+y|)*((|z|+|x+y+z|)-|x+y|)+((|y|+|z|)-|y+z|)*((|x|+|x+y+z|)-|y+z|)+((|x|+|z|)-|x+z|)*((|y|+|x+y+z|)-|x+z|),
{
    ring,
},
rw fact' at inequality,
rw ← obs at inequality,
clear obs obs' hx hab habc h1 h2 h3 fact',
have fact: 0 ≤ ((|x+y+z|+|x|+|y|+|z|)-(|x+y|+|x+z|+|y+z|)),
{
  have obv: |x|+|y|+|z|+|x+y+z|=|x+y+z|+|x|+|y|+|z|,
  {
      ring,
  },
  rw obv at hsum,
  exact nonneg_of_mul_nonneg_right inequality hsum,
},
have obv: |x+y+z|+|x|+|y|+|z|=|x|+|y|+|z|+|x+y+z|,
{
    ring,
},
rw obv at fact,
exact sub_nonneg.mp fact,
},
end

end Hlawka