Zulip Chat Archive

Stream: new members

Topic: Splitting the Goal


view this post on Zulip Dev-Indra (Mar 17 2020 at 16:21):

In Theorem Proving with Lean we learn about creating sub goals by breaking up hypothesis of the form p and q. What happens if the goal is of the form p and q? For instance let's say I want to prove the following "theorem":

theorem help (u v : ) (h1: u*v = u*v) (h2: v*v  v*u) : u*v = u*v  v*v  v*u :=
begin

end

How would I prove this? I tried rw tactic but that did not work.

view this post on Zulip Shing Tak Lam (Mar 17 2020 at 16:22):

Try split

view this post on Zulip Shing Tak Lam (Mar 17 2020 at 16:23):

It turns goals of the form A ∧ B into two separate goals, A and B.

view this post on Zulip Dev-Indra (Mar 17 2020 at 16:27):

Thanks @Shing Tak Lam It works:

theorem help (u v : ) (h1: u*v = u*v) (h2: v*v  v*u) : u*v = u*v  v*v  v*u :=
begin
    split,
    refl,
    apply h2,
end

Last updated: May 08 2021 at 18:17 UTC