## Stream: new members

### Topic: Combing specialize's

#### Aniruddh Agarwal (Jun 26 2020 at 00:28):

Is there a compound form for specialize, similar to rw? I have a bunch of statements like

  specialize h n,
specialize h' n,


in a proof.

#### Jalex Stark (Jun 26 2020 at 00:31):

interesting. (i don't think what you ask for exists) can you show the proof?
tactic#specialize

#### Aniruddh Agarwal (Jun 26 2020 at 00:31):

Here:

example (hu : seq_limit u l) (hw : seq_limit w l)
(h : ∀ n, u n ≤ v n)
(h' : ∀ n, v n ≤ w n) : seq_limit v l :=
begin
intros ε hε,
cases hu ε hε with N hN,
cases hw ε hε with M hM,
use (max N M),
intros n hn,
specialize hN n (le_of_max_le_left hn),
specialize hM n (le_of_max_le_right hn),
rw [abs_le] at *,
specialize h n,
specialize h' n,
split; linarith,
end


#### Jalex Stark (Jun 26 2020 at 00:32):

what are u, l, w?

#### Aniruddh Agarwal (Jun 26 2020 at 00:33):

real-valued sequences. you can find a compiling version of this (sans the proof) here: https://github.com/leanprover-community/tutorials/blob/master/src/exercises/05_sequence_limits.lean#L149

u, v and w are sequences and l is a real number

#### Aniruddh Agarwal (Jun 26 2020 at 00:35):

I'm just trying to shave a couple of lines off of my proof :)

#### Aniruddh Agarwal (Jun 26 2020 at 00:44):

Actually, I can do this:

example (hu : seq_limit u l) (hw : seq_limit w l)
(h : ∀ n, u n ≤ v n)
(h' : ∀ n, v n ≤ w n) : seq_limit v l :=
begin
intros ε hε,
cases hu ε hε with N hN,
cases hw ε hε with M hM,
use (max N M),
intros n hn,
specialize hN n (le_of_max_le_left hn),
specialize hM n (le_of_max_le_right hn),
rw abs_le at *,
split; linarith[h n, h' n],
end


Last updated: May 10 2021 at 19:16 UTC