One of many pattern match hygiene

Stream: general

[Scott Viteri]

Suppose I have some predicate P and tactic t1 and t2 such that

lemma l : ∀ (o₁ o₂ o₃ : option ℕ), P o₁ o₂ o₃
| none _ _ := by t₁
| _ none _ := by t₁
| _ _ none := by t₁
| (some a) (some b) (some c) := by t₂

I would like to condense the proof so that it looks like:

lemma l : ∀ (o₁ o₂ o₃ : option ℕ), P o₁ o₂ o₃
| one_is_none case := by t₁
| (some a) (some b) (some c) := by t₂

[Scott Viteri]

Is this possible/recommended?

[Yakov Pechersky]

... :=
begin
  rintro (_ | _) (_ | _) (_ | _);
  { t₁ <|> t₂ }
end

[Scott Viteri]

This is nice thank you

[Scott Viteri]

for long t1 and t2 I am finding this makes the proof less readable

[Scott Viteri]

not sure what to do about that

[Mario Carneiro]

For more targeted calls I would do this:

lemma l (o₁ o₂ o₃ : option ℕ) : P o₁ o₂ o₃ :=
begin
  cases o₁ with a, swap,
  cases o₂ with b, swap,
  cases o₃ with b, swap,
  { t₂ },
  all_goals {
    t₁
  }
end

[Eric Wieser]

Could also use tactic#case to pull out just the some some some goal without the swaps

[Yakov Pechersky]

lemma l : ∀ (o₁ o₂ o₃ : option ℕ), P o₁ o₂ o₃ :=
begin
  repeat { all_goals { rintro (_ | _) }, swap },
  t1,
  all_goals { t2 }
end

[Yakov Pechersky]

For your "variadic" needs