# Zulip Chat Archive

## Stream: new members

### Topic: Induction on something not in local context

#### Riccardo Brasca (Oct 24 2020 at 15:05):

Let us suppose I have two predicates `a : polynomial ℤ → Prop`

and `b: polynomial ℤ → Prop`

and I want to prove that `a`

implies `b`

, so the lemma would be `lemma example (p : polynomial ℤ) : a p → b p`

. How can I write a proof of something like this by induction on `p.nat_degree`

? I mean, `p.nat_degree`

does not appear in `a`

or in `b`

, so `induction p.nat_degree`

does not work.

Something better is `cases hd : p.nat_degree with d`

, it gives two goal, when `p.nat_degree = 0`

and `p.nat_degree = d + 1`

, but there is no induction hypothesis regarding `a → b`

. I see the reason: formally speaking, what I want to prove by induction is `lemma example (p : polynomial ℤ) (d : ℕ) (hd : d = p.nat_degree) : a p → b p`

, but it very strange to state the theorem this way. So what is the best way of doing it? I tried to play with `set d := p.nat_degree with hd`

and `revert hd`

but it didn't worked.

Thanks!

#### Reid Barton (Oct 24 2020 at 15:08):

What generally happens is that I suggest writing something like your `example`

as an auxiliary lemma and then applying it to `d = _`

and `hd = rfl`

, and then Mario points out that the `blah`

tactic does exactly this automatically, but I can never remember what `blah`

is.

#### Riccardo Brasca (Oct 24 2020 at 15:09):

Indeed my real question is what tactic does it automatically, I guess there is one :D

#### Reid Barton (Oct 24 2020 at 15:09):

It should be some variation on `induction`

and `generalizing`

though, so since you now understand exactly what tactic state you want to see after the tactic, you can experiment until you find it.

#### Riccardo Brasca (Oct 24 2020 at 15:13):

Ah, `generalize' hd : p.nat_degree = d`

produces the hypothesis I want, then it suffices `revert hd`

.

#### Reid Barton (Oct 24 2020 at 15:14):

If you use `induction d`

next then I bet you can skip `revert`

even.

#### Riccardo Brasca (Oct 24 2020 at 15:16):

Yes! (I need strong induction, so I think I have to use `revert`

, but it doesn't matter.)

#### Yury G. Kudryashov (Oct 24 2020 at 16:16):

See the first line of the proof of src#continuous_equiv_fun_basis

#### Yury G. Kudryashov (Oct 24 2020 at 16:18):

`unfreezingI`

is needed to unfreeze `[fintype ι]`

instance; probably not required in your case.

#### Yury G. Kudryashov (Oct 24 2020 at 16:19):

tactic#induction says:

`induction h : t`

will introduce an equality of the form`h : t = C x y`

, asserting that the input term is equal to the current constructor case, to the context.

Last updated: May 11 2021 at 21:10 UTC