Logic puzzle from John P. Pratt in Lean (starts at line 38)

pratt.lean

import tactic.interactive
import tactic.linarith

@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith

constant only_child : people → Prop
constant salary : people → ℕ

@[derive decidable_eq]
inductive job : Type | doctor | lawyer | teacher
constant P : job → people
constant J : people → job
axiom JP : ∀ (p : people) (j : job) , J p = j ↔ P j = p

lemma contradicts {p p' j} 
  (hp : J p = j) (hp' : J p' = j) (H : (p ≠ p') . tactic.interactive.trivial) : false :=
begin
  apply H,
  rw JP at hp,
  rwa [JP, hp] at hp'
end

namespace tactic.interactive
open tactic
open interactive (parse)
open lean.parser (ident)

meta def absurd_from (h1 : parse ident) (h2 : parse ident) : tactic unit :=
do H1 ← get_local h1,
   H2 ← get_local h2,
   exfalso,
   `[exact contradicts %%H1 %%H2]

end tactic.interactive
open people job

/- The exercise starts here.
  Objects of type job are either teacher, lawyer or doctor
  Objects of type people are either Smith, Brown or Jones
  J : people → job 
  P : job → people
  satisfy the following axiom which ensures that every people has only one job :
  JP : ∀ (p : people) (j : job) , J p = j ↔ P j = p
  If your context contains assumptions
  H  : J p  = j
  H' : J p' = j
  with p ≠ p' then you can use tactic 
  absurd_from H H'
  to close any goal

  For every people p, the tactic
  cases H : J p
  will open three new goals under all three possible assumptions H for the value of J p

  Remember tactics:
  * trivial will close trivial goals ;
  * exfalso will replace any goal with false. This is a good move when the
    current assumptions are inconsistent ;
  * linarith will handle easy inequality arguments.
 -/

example 
 (h₁ : only_child (P teacher)) 
 (h₂ : salary (P teacher) < salary (P lawyer))
 (h₃ : salary (P teacher) < salary (P doctor))
 (h₄ : ¬ only_child Brown)
 (h₅ : salary Smith > salary (P lawyer))
: J Smith = doctor ∧ J Brown = lawyer ∧ J Jones = teacher:=
begin
cases H : J Smith,
{ split, trivial,
  cases H' : J Brown,
  { absurd_from H H' },
  { split, trivial,
    cases H'' : J Jones,
    { absurd_from H H'' },
    { absurd_from H' H'' },
    { trivial } },
  { exfalso,
    rw JP at H',
    rw ← H' at h₄,
    exact h₄ h₁ } },
{ exfalso,
  rw JP at H,
  rw H at h₅,
  linarith },
{ exfalso,
  rw JP at H,
  rw H at h₂,
  linarith }
end