Functional extensionality

Stream: new members

[Ken Roe]

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
    ∀ (a:t→u) (b:t→u), a=b → (λ (x:t), a)=(λ (x:t), b) := sorry.

[Chris Hughes]

There's funext, but that's not the same as what you stated. The proof of the theorem you stated is assume a b h, by rw h

[Ken Roe]

Thanks. I'm running into another issue. It seems I cannot rewrite if meta variables are involved. How is the following theorem completed (ignore the "admit"--I'd like to get the "rw h" to work.

theorem dd : (λ (x:ℕ), x*2)=(λ (x:ℕ), x+x) := begin
    have h:∀ x, x*2=x+x, intro, admit,
    rw h
end

[Simon Hudon]

You can't rewrite bound variables. Use simp only [h] instead

[Simon Hudon]

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
    ∀ (a:t→u) (b:t→u), a=b → (λ (x:t), a)=(λ (x:t), b) := sorry

Isn't that normal rewriting?