## Stream: general

### Topic: One of many pattern match hygiene

#### Scott Viteri (Mar 19 2021 at 20:48):

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 (Mar 19 2021 at 20:48):

Is this possible/recommended?

#### Yakov Pechersky (Mar 19 2021 at 20:51):

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


#### Scott Viteri (Mar 19 2021 at 21:03):

This is nice thank you

#### Scott Viteri (Mar 19 2021 at 21:03):

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

#### Scott Viteri (Mar 19 2021 at 21:03):

not sure what to do about that

#### Mario Carneiro (Mar 19 2021 at 22:10):

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 (Mar 19 2021 at 22:12):

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

#### Yakov Pechersky (Mar 19 2021 at 22:27):

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