From 309f12da6f075c0ec35f8799be7c9688ed7bb7f2 Mon Sep 17 00:00:00 2001
From: pingu <nor@acorneroftheweb.com>
Date: Thu, 30 Jan 2025 20:04:53 +0100
Subject: [PATCH] You can open the namespaces

---
 Example.lean | 64 +++++++++++++++++++++++++++-------------------------
 1 file changed, 33 insertions(+), 31 deletions(-)

diff --git a/Example.lean b/Example.lean
index 0ed7026..3e7c314 100644
--- a/Example.lean
+++ b/Example.lean
@@ -1,3 +1,5 @@
+open Or
+open False renaming elim → negelim
 variable (p q r : Prop)
 
 -- commutativity of ∧ and ∨
@@ -6,11 +8,11 @@ example : p ∧ q ↔ q ∧ p :=
 
 example : p ∨ q ↔ q ∨ p :=
   ⟨λ
-    | Or.inl p => Or.inr p
-    | Or.inr q => Or.inl q,
+    | inl p => inr p
+    | inr q => inl q,
    λ
-    | Or.inl q => Or.inr q
-    | Or.inr p => Or.inl p⟩
+    | inl q => inr q
+    | inr p => inl p⟩
 
 -- associativity of ∧ and ∨
 example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
@@ -18,31 +20,31 @@ example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
 
 example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
   ⟨λ
-    | 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,
+    | inr r => inr (inr r)
+    | inl (inr q) => inr (inl q)
+    | inl (inl p) => 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⟩
+    | inl p => inl (inl p)
+    | inr (inl q) => inl (inr q)
+    | inr (inr r) => inr r⟩
 
 -- distributivity
 example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
   ⟨λ
-    | ⟨p, Or.inl q⟩ => Or.inl ⟨p,q⟩
-    | ⟨p, Or.inr r⟩ => Or.inr ⟨p,r⟩,
+    | ⟨p, inl q⟩ => inl ⟨p,q⟩
+    | ⟨p, inr r⟩ => inr ⟨p,r⟩,
   λ
-    | Or.inl ⟨p,q⟩ => ⟨p,Or.inl q⟩
-    | Or.inr ⟨p,r⟩ => ⟨p,Or.inr r⟩⟩
+    | inl ⟨p,q⟩ => ⟨p,inl q⟩
+    | inr ⟨p,r⟩ => ⟨p,inr r⟩⟩
 
 example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
   ⟨λ
-    | Or.inl p => ⟨Or.inl p, Or.inl p⟩
-    | Or.inr ⟨q,r⟩ => ⟨Or.inr q, Or.inr r⟩,
+    | inl p => ⟨inl p, inl p⟩
+    | inr ⟨q,r⟩ => ⟨inr q, inr r⟩,
   λ
-    | ⟨Or.inr q, Or.inr r⟩ => Or.inr ⟨q,r⟩
-    | ⟨Or.inl p,        _⟩ => Or.inl p
-    | ⟨       _, Or.inl p⟩ => Or.inl p⟩
+    | ⟨inr q, inr r⟩ => inr ⟨q,r⟩
+    | ⟨inl p,        _⟩ => inl p
+    | ⟨       _, inl p⟩ => inl p⟩
 
 -- other properties
 example : (p → (q → r)) ↔ (p ∧ q → r) :=
@@ -50,20 +52,20 @@ example : (p → (q → r)) ↔ (p ∧ q → r) :=
 
 example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
   ⟨
-    λ f =>  ⟨λ p => f (Or.inl p), λ q => f (Or.inr q)⟩,
+    λ f =>  ⟨λ p => f (inl p), λ q => f (inr q)⟩,
     λ
-      |⟨f, _⟩, Or.inl p => f p
-      |⟨_, g⟩, Or.inr q => g q⟩
+      |⟨f, _⟩, inl p => f p
+      |⟨_, g⟩, inr q => g q⟩
 
 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
-  ⟨λ f => ⟨λ p => f (Or.inl p), λ q => f (Or.inr q)⟩,
+  ⟨λ f => ⟨λ p => f (inl p), λ q => f (inr q)⟩,
    λ
-    | ⟨np, _⟩, Or.inl p => np p
-    | ⟨_ ,nq⟩, Or.inr q => nq q⟩
+    | ⟨np, _⟩, inl p => np p
+    | ⟨_ ,nq⟩, inr q => nq q⟩
 
 example : ¬p ∨ ¬q → ¬(p ∧ q)
-  | Or.inl np, ⟨p,_⟩ => np p
-  | Or.inr nq, ⟨_,q⟩ => nq q
+  | inl np, ⟨p,_⟩ => np p
+  | inr nq, ⟨_,q⟩ => nq q
 
 example : ¬(p ∧ ¬p) :=
   λ ⟨p,np⟩ => np p
@@ -75,14 +77,14 @@ example : ¬p → (p → q) :=
   λ np p => absurd p np
 
 example : (¬p ∨ q) → (p → q)
-  | (Or.inl np), p => absurd p np
-  | (Or.inr q), _ => q
+  | (inl np), p => absurd p np
+  | (inr q), _ => q
 
 example : p ∨ False ↔ p :=
-  ⟨λ h => Or.elim h id False.elim, λ p => Or.inl p⟩
+  ⟨λ h => elim h id negelim, λ p => inl p⟩
 
 example : p ∧ False ↔ False :=
-  ⟨λ ⟨_,f⟩ => f, λ f => False.elim f⟩
+  ⟨λ ⟨_,f⟩ => f, λ f => negelim f⟩
 
 example : (p → q) → (¬q → ¬p) :=
  λ f nq p => absurd (f p) nq