variables p q : Prop -- 1ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from and.intro (and.right h) (and.left h)) (assume h : q ∧ p, show p ∧ q, from and.intro (and.right h) (and.left h)) -- 2ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from ⟨h.right, h.left⟩) (assume h : q ∧ p, show p ∧ q, from ⟨h.right, h.left⟩) -- 3ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, ⟨h.right, h.left⟩) (assume h : q ∧ p, ⟨h.right, h.left⟩) -- 4ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (λ h, ⟨h.right, h.left⟩) (λ h, ⟨h.right, h.left⟩) -- 5ª demostración example : p ∧ q ↔ q ∧ p := ⟨λ h, ⟨h.right, h.left⟩, λ h, ⟨h.right, h.left⟩⟩