title: How to simplify a proof by induction in Lean?
body: <p>I'd like to simplify a proof by induction in Lean.</p>
  
  <p>I've defined an inductive type with 3 constructors in Lean and a binary relation on this type. I've included the axioms because Lean wouldn't let me have them as constructors for rel.</p>
  
  <pre><code>
  inductive Fintype : Type
  | a : Fintype
  | b : Fintype
  | c : Fintype
  
  inductive rel : Fintype → Fintype →  Prop 
  | r1 : rel Fintype.a Fintype.b
  | r2 : ∀ p : Prop, (p → rel Fintype.a Fintype.c )
  | r3 : ∀ p : Prop, (¬ p → rel Fintype.c Fintype.b) 
  
  
  axiom asymmetry_for_Fintype : ∀ x y : Fintype, rel x y → ¬ rel y x
  axiom trivial1 : ¬ rel Fintype.c Fintype.a
  axiom trivial2 : ¬ rel Fintype.b Fintype.c
  axiom trivial3 : ∀ p : Prop, rel Fintype.a Fintype.c → p 
  axiom trivial4 : ∀ p : Prop, rel Fintype.c Fintype.b → ¬ p
  
  </code></pre>
  
  <p>A goal was to prove the following theorem:</p>
  
  <pre><code>def nw_o_2 (X : Type) (binrel : X → X → Prop) (x y : X) : Prop := ¬ binrel y x
  def pw_o_2 (X : Type) (binrel : X → X → Prop )(x y : X) : Prop := ∀ z : X, (binrel z x → binrel z y) ∧ (binrel y z → binrel x z)
  
  theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=
  
  </code></pre>
  
  <p>I've proved it by induction on x, y, and z; the "z" comes from the definition of pw_o_2 above. But the proof is quite long (~136 lines). Is there another way to have a shorter proof?</p>