## Stream: new members

### Topic: cases with doesn't rename

#### Horatiu Cheval (Mar 13 2021 at 10:48):

I encountered situations when cases h with h1 h2 ... doesn't rename the introduced hypotheses as I would expect. For example:

inductive type
| zero : type
| arrow : type → type → type

infixr ↣ : 50 := type.arrow

inductive preterm
| var : ℕ → preterm
| app : preterm → preterm → preterm

inductive wt  : preterm → type → Prop
| var : ∀ (x : ℕ), wt (preterm.var x) type.zero
| app : ∀ (ρ σ : type) (t u : preterm), wt t (ρ ↣ σ) → wt u ρ → wt (t.app u) σ

example (t : preterm) (τ : type) : wt t τ → false  :=
begin
intros h,
induction t,
case app: u v ihu ihv
{ cases h, /-breaks h in h_ρ h_ᾰ_1 h_ᾰ-/ }
end


I thought cases h with σ h1 h2 would rename the three introduced hypotheses, in this order, but it actually only replaces h_ρ with h1 (so the first one with second one), leaving the rest unchanged. What's happening here? How can I give names to the hypotheses?

#### Eric Wieser (Mar 13 2021 at 11:47):

Not your question, but something your example raises - it looks like the lean server puts the error message on the case when it should probably put it on the }. Is this easy to fix?

#### Eric Wieser (Mar 13 2021 at 11:48):

cases h with x p σ t u ht hu works

#### Mario Carneiro (Mar 14 2021 at 05:31):

Eric Wieser said:

Not your question, but something your example raises - it looks like the lean server puts the error message on the case when it should probably put it on the }. Is this easy to fix?

Not really. It is the case tactic that fails, and } is part of the syntax of case, not a separate tactic like with { tacs .. } where braces represent a separate syntax form that can be treated specially

Last updated: May 14 2021 at 06:16 UTC