Zulip Chat Archive

Stream: general

Topic: proofs

Emma Mitchell (Apr 26 2020 at 23:28):

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 (Apr 26 2020 at 23:29):

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

Emma Mitchell (Apr 26 2020 at 23:32):

i have not

Kevin Buzzard (Apr 26 2020 at 23:37):

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

Last updated: Aug 03 2023 at 10:10 UTC