Tutorial Proof 0035

Stream: new members

[leafGecko]

Hi all, I was trying to follow the tutorial on github, this is ID 0035 in the 05_sequence_limit file, where I am asked to prove squeeze theorem.

/- Let's do something similar: the squeezing theorem. -/
-- 0035
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
  unfold seq_limit,
  intros εg εgg0,
  cases hu (εg / 2) (by linarith) with N1 hu,
  cases hw (εg / 2) (by linarith) with N2 hw,
  have Nt := max N1 N2,
  use Nt,
  intros tx txgNt,
  rw ge_max_iff at txgNt, -- WRONG
end

But rw failed at the penultimate line. It seems like Lean does not know Nt is max N1 N2.
What I would like is an abstraction feel, similar to use def, so that Nt can be expanded to max N1 N2. How shall I do that?

Thanks!

[Kevin Buzzard]

Change have to let and you should be fine.

[Kevin Buzzard]

Even better, you could use set Nt := max N1 N2 with hNt and then you can rw hNt if you want to change Nt to its definition.

[Ruben Van de Velde]

Or even use

use max N1 N2,

[leafGecko]

Thanks! And by the way, if I have

abs_le (x y : ℝ) : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y
H: |a| <= |b|

then why does have H2 := abs_le.1 H work but not have H2 := abs_le.1 _ _ H?
I thought abs_le.1 lead to (x y: R): |x| <= y -> -y <= x /\ x <= y...

[Kevin Buzzard]

What's the error?

[Kevin Buzzard]

(ps have is correct here -- you use have for proofs and let for data like real numbers, that's why your original code doesn't work)

[leafGecko]

Kevin Buzzard said:

What's the error?

function expected at
  abs_le.mp ?m_7
term has type
  -?m_4 ≤ ?m_5 ∧ ?m_5 ≤ ?m_4

[Kevin Buzzard]

abs_le.1 doesn't lead to what you say -- that would be (abs_le _ _).1 (the .1 only applies to the iff bit) (Edit: this comment was made assuming the incorrect claim that x and y were explicit in abs_le)

[Kevin Buzzard]

I am surprised that have H2 := abs_le.1 H works if abs_le is defined the way you say it is.

[leafGecko]

That makes sense :D

[leafGecko]

image.png

[Ruben Van de Velde]

It's mathlib docs#add_le, which takes {a b}

[Kevin Buzzard]

So the reason it doesn't work with the _s is because Lean is not expecting the inputs to be explicit.

[Kevin Buzzard]

Super-quick Patrick has updated the tutorial project so that now the variables are implicit in the comment.