# Zulip Chat Archive

## Stream: general

### Topic: apply induction_lemma, clear n

#### Kevin Buzzard (Nov 11 2020 at 19:44):

Reviewing a PR and I see `apply nat.strong_induction_on n, clear n,`

. This reminded me of some code I was writing last week which had the line `apply span_induction hx; clear hx x,`

. This is perhaps quite a common idiom? The reason one wants to clear the variable is because one is about to embark on a proof or proofs of results related to the original goal and ones instinct is to use the same variable names again -- for example I want to prove results about elements of submodules and I want to use x and y for these elements, so it's annoying if I don't clear the original `x`

which is now useless to me. Is this style OK or is it worth modding some induction tactic to make this happen automatically? I'm not entirely sure what I want here, but given that I've now seen this twice in one week it made me wonder.

#### Mario Carneiro (Nov 11 2020 at 20:29):

I think ssreflect has something for this, a la `have {h1} h2 := foo h1`

which is like ` have h2 := foo h1, clear h1`

except it works even if you reuse the variable names

#### Mario Carneiro (Nov 11 2020 at 20:33):

I don't see how we can offer something better than `; clear`

though

#### Mario Carneiro (Nov 11 2020 at 20:33):

in the examples, `apply span_induction hx clearing hx x`

would be no better

#### Shing Tak Lam (Nov 11 2020 at 20:41):

fwiw `induction n using nat.strong_induction_on with n hn`

works (does the same as `apply nat.strong_induction_on n, clear n, intros n hn`

)

#### Kevin Buzzard (Nov 11 2020 at 21:42):

Yes, I realised when I was posting that I couldn't really see a solution which would be saving too many characters!

Last updated: May 15 2021 at 23:13 UTC