diff --git a/Example.lean b/Example.lean
index 99b94d2..311e88c 100644
--- a/Example.lean
+++ b/Example.lean
@@ -1,133 +1,81 @@
 variable (p q r : Prop)
 
 -- commutativity of ∧ and ∨
-example : p ∧ q ↔ q ∧ p := by
-  apply Iff.intro
-  · intro pandq
-    apply And.intro
-    · apply And.right pandq
-    · apply And.left pandq
-  · intro qandp
-    apply And.intro
-    · apply And.right qandp
-    · apply And.left qandp
+example : p ∧ q ↔ q ∧ p :=
+  Iff.intro (λ ⟨p,q⟩ => ⟨q,p⟩) (λ ⟨q,p⟩ => ⟨p,q⟩)
 
-example : p ∨ q ↔ q ∨ p := by
-  apply Iff.intro
-  · intro porq
-    cases porq with
-    | inl p => exact Or.inr p
-    | inr q => exact Or.inl q
-  · intro qorp
-    cases qorp with
-    | inl q => exact Or.inr q
-    | inr p => exact Or.inl p
+example : p ∨ q ↔ q ∨ p :=
+  Iff.intro
+    (λ
+      | Or.inl p => Or.inr p
+      | Or.inr q => Or.inl q)
+    (λ
+      | Or.inl q => Or.inr q
+      | Or.inr p => Or.inl p)
 
 -- associativity of ∧ and ∨
-example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
-  apply Iff.intro
-  · intro pqandr
-    apply And.intro
-    · exact And.left (And.left pqandr)
-    · apply And.intro
-      · exact And.right (And.left pqandr)
-      · exact And.right pqandr
-  · intro pandqr
-    apply And.intro
-    · apply And.intro
-      · exact And.left pandqr
-      · exact And.left (And.right pandqr)
-    ·  exact And.right (And.right pandqr)
+example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
+  Iff.intro
+    (λ ⟨⟨p,q⟩,r⟩ => ⟨p,⟨q,r⟩⟩)
+    (λ ⟨p,⟨q,r⟩⟩ => ⟨⟨p,q⟩,r⟩)
 
-example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
-  apply Iff.intro
-  · intro pqorr
-    cases pqorr with
-    | inr r => apply Or.inr (Or.inr r)
-    | inl porq => cases porq with
-      | inl p => apply Or.inl p
-      | inr q => apply Or.inr (Or.inl q)
-  · intro porqr
-    cases porqr with
-    | inl p => apply Or.inl (Or.inl p)
-    | inr qorr => cases qorr with
-      | inr r => apply Or.inr r
-      | inl q => apply Or.inl (Or.inr q)
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
+  Iff.intro
+  (λ
+    | Or.inr r => Or.inr (Or.inr r)
+    | Or.inl (Or.inr q) => Or.inr (Or.inl q)
+    | Or.inl (Or.inl p) => Or.inl p)
+  (λ
+    | Or.inl p => Or.inl (Or.inl p)
+    | Or.inr (Or.inl q) => Or.inl (Or.inr q)
+    | Or.inr (Or.inr r) => Or.inr r)
 
 -- distributivity
-example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
-  apply Iff.intro
-  · intro pandqorr
-    cases pandqorr with
-    | intro p qor => cases qor with
-      | inl q => apply Or.inl (And.intro p q)
-      | inr r => apply Or.inr (And.intro p r)
-  · intro pandqorpandr
-    cases pandqorpandr with
-    | inl pandq => apply And.intro (And.left pandq) (Or.inl (And.right pandq))
-    | inr pandr => apply And.intro (And.left pandr) (Or.inr (And.right pandr))
+example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
+  Iff.intro
+  (λ
+    | ⟨p, Or.inl q⟩ => Or.inl ⟨p,q⟩
+    | ⟨p, Or.inr r⟩ => Or.inr ⟨p,r⟩)
+  (λ
+    | Or.inl ⟨p,q⟩ => ⟨p,Or.inl q⟩
+    | Or.inr ⟨p,r⟩ => ⟨p,Or.inr r⟩)
 
-example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
-  apply Iff.intro
-  · intro porqandr
-    cases porqandr with
-    | inl p => apply And.intro (Or.inl p) (Or.inl p)
-    | inr qandr => apply And.intro (Or.inr (And.left qandr)) (Or.inr (And.right qandr))
-  · intro porqandporr
-    cases And.left porqandporr with
-    | inl p => apply Or.inl p
-    | inr q => cases And.right porqandporr with
-      | inl p => apply Or.inl p
-      | inr r => apply Or.inr (And.intro q r)
+example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
+  Iff.intro
+  (λ
+    | Or.inl p => ⟨Or.inl p, Or.inl p⟩
+    | Or.inr ⟨q,r⟩ => ⟨Or.inr q, Or.inr r⟩)
+  (λ
+    | ⟨Or.inr q, Or.inr r⟩ => Or.inr ⟨q,r⟩
+    | ⟨Or.inl p,        _⟩ => Or.inl p
+    | ⟨       _, Or.inl p⟩ => Or.inl p)
 
 -- other properties
-example : (p → (q → r)) ↔ (p ∧ q → r) := by
-  apply Iff.intro
-  · intro ptoqtor
-    intro pandq
-    exact ptoqtor (And.left pandq) (And.right pandq)
-  · intro pandqtor
-    intro p
-    intro q
-    exact pandqtor (And.intro p q)
+example : (p → (q → r)) ↔ (p ∧ q → r) :=
+  Iff.intro
+    (λ f ⟨p,q⟩ => f p q)
+    (λ f p q => f ⟨p,q⟩)
 
-example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
-  apply Iff.intro
-  · intro porqtor
-    apply And.intro
-    · intro p
-      exact porqtor (Or.inl p)
-    · intro q
-      exact porqtor (Or.inr q)
-  · intro ptorandqtor
-    intro porq
-    cases porq with
-    | inl p => exact (And.left ptorandqtor) p
-    | inr q => exact (And.right ptorandqtor) q
+example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
+  Iff.intro
+    (λ porqtor => And.intro (λ p => porqtor (Or.inl p)) (λ q => porqtor (Or.inr q)))
+    (λ
+      |⟨f, _⟩, Or.inl p => f p
+      |⟨_, g⟩, Or.inr q => g q)
 
-example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
-  apply Iff.intro
-  · intro nporq
-    apply And.intro
-    · intro p
-      exact nporq (Or.inl p)
-    · intro q
-      exact nporq (Or.inr q)
-  · intro npandnq
-    intro porq
-    cases porq with
-    | inl p => exact (And.left npandnq) p
-    | inr q => exact (And.right npandnq) q
+example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
+  Iff.intro
+    (λ nporq => And.intro (λ p => nporq (Or.inl p)) (λ q => nporq (Or.inr q)))
+    (λ
+      | ⟨np, _⟩, Or.inl p => np p
+      | ⟨_ ,nq⟩, Or.inr q => nq q)
 
-example : ¬p ∨ ¬q → ¬(p ∧ q) := by
-  intro npornq
-  cases npornq with
-  | inl np => intro pandq; exact np (And.left pandq)
-  | inr nq => intro pandq; exact nq (And.right pandq)
+example : ¬p ∨ ¬q → ¬(p ∧ q)
+  | Or.inl np, ⟨p,_⟩ => np p
+  | Or.inr nq, ⟨_,q⟩ => nq q
 
-example : ¬(p ∧ ¬p) := by
-  intro pandnp
-  exact (And.right pandnp) (And.left pandnp)
+example : ¬(p ∧ ¬p) :=
+  λ ⟨p,np⟩ => np p
 
 example : p ∧ ¬q → ¬(p → q) :=
   λ ⟨p,nq⟩ ptoq => nq (ptoq p)
@@ -139,21 +87,11 @@ example : (¬p ∨ q) → (p → q)
   | (Or.inl np), p => absurd p np
   | (Or.inr q), _ => q
 
-example : p ∨ False ↔ p := by
-  apply Iff.intro
-  · intro porf
-    apply Or.elim porf id False.elim
-  · intro p
-    apply Or.inl p
-
-
-example : p ∧ False ↔ False := by
-  apply Iff.intro
-  · intro ⟨p,f⟩
-    exact f
-  · intro f
-    apply False.elim f
+example : p ∨ False ↔ p :=
+  Iff.intro (λ porf => Or.elim porf id False.elim) (λ p => Or.inl p)
 
+example : p ∧ False ↔ False :=
+  Iff.intro (λ ⟨_,f⟩ => f) (λ f => False.elim f)
 
 example : (p → q) → (¬q → ¬p) :=
  λ ptoq nq p => absurd (ptoq p) nq