## Stream: new members

### Topic: Splitting the Goal

#### 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.

#### Shing Tak Lam (Mar 17 2020 at 16:22):

Try split

#### Shing Tak Lam (Mar 17 2020 at 16:23):

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

#### 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