kenny.lean

import data.nat.prime
import tactic

open nat

lemma thing' {a b c : ℕ} (ha : 0 < a) (hab : a < b) (hbc : b < c)
  (recip : (a : ℚ)⁻¹ + (b : ℚ)⁻¹ + (c : ℚ)⁻¹ = 1) :
  prime (a + b + c) :=
begin
  cases lt_or_ge a 3,
  { interval_cases a,
    { exfalso,
      simp only [cast_one, inv_one] at recip,
      rw [add_assoc, add_eq_left_iff] at recip,
      apply ne_of_gt (add_pos _ _) recip;
      rw inv_pos;
      norm_cast;
      linarith },
    { rw [←eq_sub_iff_add_eq', ←sub_sub] at recip,
      norm_num at recip,
      rw [one_div, inv_eq_iff, inv_sub_inv, inv_div] at recip,
      { have b_lt_c : (b : ℚ) < c,
        { assumption_mod_cast },
        rw ←recip at b_lt_c,
        have b_lt_four : b < 4,
        { rw [lt_div_iff, mul_comm, mul_lt_mul_right, sub_lt_iff_lt_add] at b_lt_c,
          { assumption_mod_cast },
          { norm_cast,
            apply lt_trans ha hab },
          { rw sub_pos,
            assumption_mod_cast } },
        interval_cases b,
        norm_num at recip,
        norm_cast at recip,
        subst c,
        norm_num },
      { linarith },
      { norm_cast,
        apply ne_of_gt (ha.trans hab) } } },
  { have inv_b_lt : (b : ℚ)⁻¹ < 3⁻¹,
    { rw inv_lt_inv (show 0 < (b : ℚ), by norm_num; linarith) (show 0 < (3 : ℚ), by norm_num),
      norm_cast,
      apply lt_of_le_of_lt h hab },
    have inv_c_lt : (c : ℚ)⁻¹ < 3⁻¹,
    { rw inv_lt_inv (show 0 < (c : ℚ), by norm_num; linarith) (show 0 < (3 : ℚ), by norm_num),
      norm_cast,
      linarith },
    have inv_a_le : (a : ℚ)⁻¹ ≤ 3⁻¹,
    { apply inv_le_inv_of_le (show 0 < (3 : ℚ), by norm_num),
      assumption_mod_cast },
    have := add_lt_add (add_lt_add_of_le_of_lt inv_a_le inv_b_lt) inv_c_lt,
    rw recip at this,
    norm_num at this },
end

lemma thing {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
  (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
  (recip : (a : ℚ)⁻¹ + (b : ℚ)⁻¹ + (c : ℚ)⁻¹ = 1) :
  prime (a + b + c) :=
begin
  wlog hab' : a < b := lt_or_gt_of_ne hab using a b,
  wlog : a < b ∧ b < c using [a b c, a c b, c a b],
  { refine or.imp (and.intro hab') (λ t, _) (lt_or_gt_of_ne hbc),
    refine or.imp (λ z, ⟨z, t⟩) (λ z, ⟨z, hab'⟩) (lt_or_gt_of_ne hac) },
  { apply thing' ha hab' case.2 recip },
end