2. Swap a conjunction

EasyProofFree10 points

Prove that a conjunction can be read in either order: from a proof of P ∧ Q, build a proof of Q ∧ P.

Solution.lean

1theorem solution (P Q : Prop) : P ∧ Q → Q ∧ P := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P Q:Prop

⊢P ∧ Q → Q ∧ P

ReadyLn 1, Col 1Lean 4

Draft saved in this browser