import Mathlib

#check True ∨ False  -- type check expression
#eval  True ∨ False  -- evaluate expression

/- prove the commutativity of ∧ -/

#check and_comm

theorem my_and_comm : (p : Prop) → (q : Prop) → p ∧ q → q ∧ p := by
  sorry
  --intro p q
  --intro h
  --obtain ⟨hp, hq⟩ := h
  --exact ⟨hq, hp⟩

theorem my_and_comm' (p : Prop) (q : Prop) (h : p ∧ q) : q ∧ p := by
  sorry
  --obtain ⟨hp, hq⟩ := h
  --exact ⟨hq, hp⟩

theorem my_and_comm'' (p : Prop) (q : Prop) (h : p ∧ q) : q ∧ p :=
  ⟨h.right, h.left⟩

-- any two proofs of the same proposition are automatically equal
theorem same_thm : my_and_comm = my_and_comm' :=
  rfl  -- a thing is equal to itself

#check and_comm

#print axioms my_and_comm
#print axioms my_and_comm'

#check 2 + 1
#eval  2 + 1

#check 3 = 2 + 1
#eval  3 = 2 + 1