leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: show 2 functions are equal


Max Glick (May 22 2022 at 14:30):

Hello, very basic question as I am finishing up the tutorial project. I have a goal u=v where u and v have function types. How do I conclude this, from say \forall n, u n = v n?

Yaël Dillies (May 22 2022 at 14:31):

You use tactic#ext

Max Glick (May 22 2022 at 14:34):

Thanks.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll