reverse implication for some \iff

ZeroToLean/LearningLean/Basic.lean

@@ -21,20 +21,32 @@ theorem p_implies_p_or_q
     intro hp
     exact Or.inl hp 
 theorem and_commutative
-  : P ∧ Q → Q ∧ P := by
+  : P ∧ Q ↔ Q ∧ P := by
-  intro hpq
+  constructor
-  cases hpq with
+  · intro hpq
-  | intro hp hq =>
+    cases hpq with
+    | intro hp hq =>
     exact ⟨hq,hp⟩
+  · intro hqp 
+    cases hqp with
+    | intro hq hp =>
+      exact ⟨hp,hq⟩
 
 theorem or_commutative
-  : P ∨ Q → Q ∨ P := by
+  : P ∨ Q ↔ Q ∨ P := by
-    intro p_or_q
+    constructor
-    cases p_or_q with
+    · intro p_or_q
-    | inl hp  =>
+      cases p_or_q with
-      exact Or.inr hp
+      | inl hp  =>
-    | inr hq =>
+        exact Or.inr hp
-      exact Or.inl hq
+      | inr hq =>
+        exact Or.inl hq
+    · intro q_or_p
+      cases q_or_p with
+      | inl hq =>
+        exact Or.inr hq
+      | inr hp =>
+        exact Or.inl hp
 
 theorem p_imples_q_and_q_implies_r_Implies_p_implies_r
   : (P→Q) ∧ (Q→R) → (P→R) := by
@@ -51,13 +63,20 @@ theorem double_negation
     exact hnotp hp
 
 theorem and_associative
-  : P ∧ (Q ∧ R) → (P ∧ Q) ∧ R := by
+  : P ∧ (Q ∧ R) ↔ (P ∧ Q) ∧ R := by
-    intro h
+    constructor
-    cases h with
+    · intro h
-    | intro p q_and_r =>
+      cases h with
-      cases q_and_r with
+      | intro p q_and_r =>
-      | intro q r =>
+        cases q_and_r with
-        exact ⟨ ⟨p,q⟩,r⟩
+        | intro q r =>
+          exact ⟨⟨p,q⟩,r⟩
+    · intro h
+      cases h with
+      | intro p_and_q r =>
+        cases p_and_q with
+        | intro p q =>
+          exact ⟨p, ⟨q,r⟩⟩
 
 theorem contrapositive
   : (P → Q) → (¬Q → ¬P) := by