Eta expansions on functions

Stream: Is there code for X?

[Arnav Sabharwal]

Is there a theorem of the form "two functions are equal iff their values across all inputs are equal"?

[Adam Topaz]

docs#funext

[Adam Topaz]

Or just the ext tactic, or the funext tactic

[Adam Topaz]

I’m not sure if we have docs#funext_iff or some other name, assuming you insist on an “iff” statement

[Adam Topaz]

Ah it’s docs#Function.funext_iff

[Arnav Sabharwal]

Thank you!