diff --git a/examples/lean/wf.lean b/examples/lean/wf.lean
index ab82f75f6..e798f706c 100644
--- a/examples/lean/wf.lean
+++ b/examples/lean/wf.lean
@@ -13,14 +13,38 @@ theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf
      obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
          -- The main "trick" is to define Q x as ¬ P x.
          -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
-         let Q   : A → Bool                               := λ x, ¬ P x,
-             Qw  : ∃ w, Q w                               := exists_intro w Hw,
-             Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b  := Hwf Q Qw
-         in obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), from Qwf,
-              -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
-              let s1 : ∀ b, R b r → P b   := take b : A, assume H : R b r,
-                                                 -- We are using Hr to derive ¬ ¬ P b
-                                                 not_not_elim (and_elimr Hr b H),
-                  s2 : P r                 := iH r s1,
-                  s3 : ¬ P r               := and_eliml Hr
-              in absurd s2 s3)
+         let Q : A → Bool  := λ x, ¬ P x in
+         have Qw  : ∃ w, Q w,
+           from exists_intro w Hw,
+         have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b,
+           from Hwf Q Qw,
+         obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
+           from Qwf,
+         -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
+         have s1 : ∀ b, R b r → P b,
+           from take b : A, assume H : R b r,
+                  -- We are using Hr to derive ¬ ¬ P b
+                  not_not_elim (and_elimr Hr b H),
+         have s2 : P r,
+           from iH r s1,
+         have s3 : ¬ P r,
+           from and_eliml Hr,
+         show false,
+           from absurd s2 s3)
+
+-- More compact proof
+theorem wf_induction2 {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x)
+                     : ∀ x, P x
+:= by_contradiction (assume N : ¬ ∀ x, P x,
+     obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
+         -- The main "trick" is to define Q x as ¬ P x.
+         -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
+         let Q : A → Bool  := λ x, ¬ P x in
+         obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
+           from Hwf Q (exists_intro w Hw),
+         -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
+         have s1 : ∀ b, R b r → P b,
+           from take b : A, assume H : R b r,
+                  -- We are using Hr to derive ¬ ¬ P b
+                  not_not_elim (and_elimr Hr b H),
+         absurd (iH r s1) (and_eliml Hr))