Two small tactics questions

Stream: new members

[nrs]

1. Is there a block tactic to chain <;>? I would like to simplify

example : (∀ x, p x ∧ q x) -> (∀ x, p x) ∧ (∀ x, q x) := by
  intro h
  constructor <;> intro x <;> specialize h x <;> cases h <;> assumption

2. Given anonymous assumptions left✝ : ∀ (x : α), p x right✝ : ∀ (x : α), q x, is there a way to apply them both to x? For example, in order to complete:

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) := by
  intro h x
  constructor <;> cases h <;> _

[Julian Berman]

example (p q : Nat → Prop) : (∀ x, p x ∧ q x) -> (∀ x, p x) ∧ (∀ x, q x) := by
  intro h
  constructor
  all_goals (intro x; specialize h x; cases h; assumption)

[nrs]

Julian Berman said:

example (p q : Nat → Prop) : (∀ x, p x ∧ q x) -> (∀ x, p x) ∧ (∀ x, q x) := by
  intro h
  constructor
  all_goals (intro x; specialize h x; cases h; assumption)

ah very neat! thanks a lot! by any chance would you know about the second question? (but already, highly appreciated for the answer to the first question!)

[Ruben Van de Velde]

Or simply

example : (∀ x, p x ∧ q x) -> (∀ x, p x) ∧ (∀ x, q x) := by
  intro h
  constructor <;>
  · intro x
    specialize h x
    cases h
    assumption

[nrs]

Ruben Van de Velde said:

Or simply

example : (∀ x, p x ∧ q x) -> (∀ x, p x) ∧ (∀ x, q x) := by
  intro h
  constructor <;>
  · intro x
    specialize h x
    cases h
    assumption

very cool! thanks!