kendall.lean

import analysis.special_functions.trigonometric

noncomputable theory
open real

lemma thingy {u : ℝ} (h : -1 ≤ u) (ha : u ≤ 1) : u ^ 2 ≤ 1 :=
begin
  have : abs u ≤ 1,
    rw abs_le, simp [h, ha],
  have : (abs u)^2 ≤ 1^2,
    apply pow_le_pow_of_le_left,
    exact abs_nonneg u,
    assumption,
  simp only [one_pow] at this,
  rw [pow_two, abs_mul_abs_self] at this,
  rwa pow_two,
end

def kendall {a b c : ℝ} (h0a : 0 < a) (hab : a ≤ b) (hbc : b ≤ c) (hcab : c < a + b) :
  arccos ((b^2 + c^2 - a^2) / (2*b*c)) + arccos ((a^2 + c^2 - b^2) / (2*a*c)) + arccos ((a^2 + b^2 - c^2) / (2*a*b)) = pi :=
begin
  let t := ((a^2 + c^2 - b^2) / (2*a*c)),
  let u := ((b^2 + c^2 - a^2) / (2*b*c)),
  let v := ((a^2 + b^2 - c^2) / (2*a*b)),
  let c₁ := ((a^2 + c^2 - b^2) / (2*c)),
  let c₂ := ((b^2 + c^2 - a^2) / (2*c)),
  have : a ≠ 0, { linarith },
  have : b ≠ 0, { linarith },
  have : c ≠ 0, { linarith },
  have : 0 < 2 * a * b,
  { apply mul_pos; linarith },
  have : 0 < 2 * a * c,
  { apply mul_pos; linarith },
  have : 0 < 2 * b * c,
  { apply mul_pos; linarith },
  have : a^2 ≠ 0, { apply pow_ne_zero 2 ‹a ≠ 0› },
  have : b^2 ≠ 0, { apply pow_ne_zero 2 ‹b ≠ 0› },
  have : c^2 ≠ 0, { apply pow_ne_zero 2 ‹c ≠ 0› },
  have : c₁ + c₂ = c,
  { change _ / _ + _ / _ = _,
    rw [← add_div, div_eq_iff],
    ring,
    linarith },
  have adds_eq : b^2 + c₁^2 = a^2 + c₂^2,
  { have : c₂ = c - c₁,
    { rw [← ‹c₁ + c₂ = c›], ring },
    rw [this, pow_two (_ - _), mul_sub, sub_mul, sub_mul, ← sub_add, mul_comm c₁, ← add_assoc,
        ← pow_two c₁, add_left_inj, sub_sub, ← two_mul],
    field_simp [(show 2 * c ≠ 0, by linarith)],
    ring },
  have : 0 ≤ b ^ 2 + c ^ 2 - a ^ 2,
  { rw add_sub_assoc, apply add_nonneg, apply pow_nonneg, linarith,
    rw sub_nonneg, apply pow_le_pow_of_le_left, linarith, linarith, },
  have : v * b * a = (a^2 + b^2 - c^2) / 2,
  { field_simp [‹a ≠ 0›, ‹b ≠ 0›], ring, },
  have : t = c₁ / a,
  { rw [div_div_eq_div_mul, mul_right_comm 2 c a] },
  have : u = c₂ / b,
  { rw [div_div_eq_div_mul, mul_right_comm 2 c b] },
  have : 0 ≤ t,
  { apply div_nonneg, rw add_sub_assoc, apply add_nonneg, apply pow_nonneg, linarith,
    rw sub_nonneg, apply pow_le_pow_of_le_left, linarith, assumption, linarith },
  have : -1 ≤ t := le_trans (show -(1 : ℝ) ≤ 0, by norm_num) ‹0 ≤ t›,
  have : t ≤ 1, { sorry },
  have : 0 ≤ u, { apply div_nonneg, assumption, linarith },
  have : -1 ≤ u := le_trans (show -(1 : ℝ) ≤ 0, by norm_num) ‹0 ≤ u›,
  have : u ≤ 1, { sorry },
  have : -1 ≤ v, { sorry },
  have : v ≤ 1, { sorry },
  have : c₂ ≤ b,
  { rwa [← div_le_one (show 0 < b, by linarith), ← ‹u = c₂ / b›] },
  have : 0 ≤ b ^ 2 - c₂ ^ 2,
  { rw sub_nonneg,
    apply pow_le_pow_of_le_left,
    apply div_nonneg,
      assumption,
    linarith,
    assumption },
  change arccos u + arccos t + arccos v = _,
  suffices : arccos v = arcsin u + arcsin t,
  { rw [arccos_eq_pi_div_two_sub_arcsin, arccos_eq_pi_div_two_sub_arcsin],
    linarith },
  apply cos_inj_of_nonneg_of_le_pi,
  { apply arccos_nonneg },
  { apply arccos_le_pi },
  { apply add_nonneg,
    apply arcsin_nonneg,
    assumption,
    apply arcsin_nonneg,
    assumption },
  { have := arcsin_le_pi_div_two u,
    have := arcsin_le_pi_div_two t,
    linarith },
  { rw [cos_arccos ‹-1 ≤ v› ‹v ≤ 1›, cos_add, cos_arcsin ‹-1 ≤ u› ‹u ≤ 1›,
        cos_arcsin ‹-1 ≤ t› ‹t ≤ 1›, sin_arcsin ‹-1 ≤ u› ‹u ≤ 1›, sin_arcsin ‹-1 ≤ t› ‹t ≤ 1›],
    rw [eq_sub_iff_add_eq, ←sqrt_mul, eq_comm, sqrt_eq_iff_mul_self_eq],
    { rw [‹t = c₁ / a›, ‹u = c₂ / b›],
      clear_value c₁ c₂,
      rw ← sub_eq_sub_iff_add_eq_add at adds_eq,
      rw [div_pow, div_pow, sub_div' _ _ _ (pow_ne_zero 2 ‹b ≠ 0›),
          sub_div' _ _ _ (pow_ne_zero 2 ‹a ≠ 0›), div_mul_eq_mul_div, mul_div_assoc',
          add_div' _ _ _ ‹b ≠ 0›, add_div' _ _ _ ‹a ≠ 0›, one_mul, one_mul, ← pow_two, div_pow,
          div_eq_iff (pow_ne_zero 2 ‹b ≠ 0›), mul_right_comm _ _ (b^2),
          div_mul_cancel _ (pow_ne_zero 2 ‹b ≠ 0›), div_pow, div_eq_iff (pow_ne_zero 2 ‹a ≠ 0›),
          mul_assoc (_ - _), div_mul_cancel _ (pow_ne_zero 2 ‹a ≠ 0›), adds_eq, ← pow_two],
      congr' 1,
      rw [‹v * b * a = _›],
      rw [←‹c₁ + c₂ = c›],
      field_simp,
      ring,
      rw [add_sub, ← sub_eq_add_neg, sub_right_comm, adds_eq],
      ring },
    { apply mul_nonneg,
      rw sub_nonneg,
      apply thingy; assumption,
      rw sub_nonneg,
      apply thingy; assumption },
    { rw [‹t = _›, ‹u = _›, mul_div_assoc', add_div' _ _ _ ‹a ≠ 0›, div_mul_eq_mul_div c₁,
          add_div' _ _ _ ‹b ≠ 0›, mul_right_comm v a b, ‹v * b * a = _›],
      apply div_nonneg _ (show 0 ≤ a, by linarith),
      apply div_nonneg _ (show 0 ≤ b, by linarith),
      rw div_add' _ _ _,
      apply div_nonneg,
      rw ← sub_eq_sub_iff_add_eq_add at adds_eq,
      rw [←‹c₁ + c₂ = c›],
      rw [pow_two (_ + _), add_mul, mul_add, mul_add, ← pow_two, ← pow_two, ← add_assoc,
          mul_comm c₂, ← sub_sub, add_assoc, ← mul_two, ← sub_sub, sub_right_comm, sub_add_cancel,
          ← sub_add_eq_add_sub, ← adds_eq],
      have := add_assoc (b^2 - c₂^2) (b^2) (- c₂^2),
      rw [← sub_eq_add_neg] at this,
      rw [this, ←sub_eq_add_neg, ← two_mul],
      apply mul_nonneg,
      norm_num,
      assumption,
      norm_num,
      norm_num },
    { rw sub_nonneg,
      apply thingy; assumption } },
end