proofs

Stream: general

[Emma Mitchell]

Hi i am new here, could someone please help me prove theses theorems. Thank you!!

theorem t7 : ∀ {P Q : Prop}, P ∧ Q ↔ Q ∧ P := _ theorem t8 {P Q R : Prop} (p2r : P → R) (q2r : Q → R) (porq : P ∨ Q) : R := _

[Kevin Buzzard]

Have you played the natural number game, or read the early chapters of Theorem Proving In Lean?

[Emma Mitchell]

i have not

[Kevin Buzzard]

There are many different ways to prove these theorems, you can explicitly construct the function, you can use low-level tactics and you can use high-level tactics. Probably by tauto! is the quickest way to solve them, but you'll have to input tactic at the top of your file