Combing specialize's

Stream: new members

[Aniruddh Agarwal]

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]

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

[Aniruddh Agarwal]

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]

what are u, l, w?

[Aniruddh Agarwal]

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]

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

[Aniruddh Agarwal]

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