Splitting the Goal

Stream: new members

[Dev-Indra]

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.

[Shing Tak Lam]

Try split

[Shing Tak Lam]

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

[Dev-Indra]

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