split tactic on AND ?

Stream: lean4

[Chris Lovett]

The NNG uses the split tactic heavily in Advanced Proposition World and in lean3 it could split P ∧ Q and P ↔ Q, but in Lean4 it cannot. Is this use of split replaced by constructor in lean4 ? For example, level 1 in lean3 is:

example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
begin
  split,
  exact p,
  exact q,
end

And I can port this as:

example (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
  constructor
  exact p
  exact q

But I can also port it to the much simpler version:

example (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
  exact ⟨ p, q ⟩

what which is preferable here? Perhaps the constructor version since it leads up to level 8 where constructor must be used to solve it.

[Mario Carneiro]

yes, split is now constructor

[Mario Carneiro]

The NNG deliberately doesn't use most features of the term language so as to show every subterm in tactic mode

[Mario Carneiro]

most NNG proofs can be (very) significantly golfed, that's not the point

[Chris Lovett]

Thanks for the confirmation, feedback welcome on my Lean 4 version of Advanced Proposition World, I've ported most of the levels but I had some trouble eliminating "term language" with level 4 and 5 involving Iff, and I'm stuck on level 8. I finally solved level 10 without cc since cc is not yet available.