split

The split tactic works on goals such as P ∧ Q or P ↔ Q. It breaks up one “compound” goal into one or more simpler goals. More formally, if the goal is a structure, that is, an inductive type with one constructor, split will turn the goal into goals asking for terms of all the types needed for the constructor.

Example (∧)

If the goal is

P Q : Prop,
⊢ P ∧ Q

then split changes this one goal into two goals, namely

P Q : Prop,
⊢ P

and

P Q : Prop,
⊢ Q

Here is a fully worked example.

try it!

example (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q :=
begin
  split,
  { -- first goal is P
    exact HP
  },
  { -- second goal is Q
    exact HQ
  }
end

Example (↔)

A term of type P ↔ Q is constructed in Lean by giving terms of type P → Q and Q → P.

try it!

example (P Q : Prop) (HPQ : P → Q) (HQP : Q → P) : P ↔ Q :=
begin
  split,
  { -- first goal is P → Q
    exact HPQ
  },
  { -- second goal is Q → P
    exact HQP
  }
end