Proving equality of functions

Stream: lean4

[Artur Chakhvadze]

I have a simple toy data type with a function

inductive Arrow
  | up
  | down

def reverse : Arrow → Arrow
  | Arrow.up => Arrow.down
  | Arrow.down => Arrow.up

I want to prove that reverse ∘ reverse = id, but I can only do it by introducing an axiom that shows that two functions are equal iff they are pointwise equal:

axiom pointwiseEquality {a b : Type} (f g : a → b) : (∀x : a, f x = g x) ↔ f = g

example : reverse ∘ reverse = id :=
  have f (a : Arrow) : (reverse ∘ reverse) a = a :=
    match a with
    | Arrow.up => rfl
    | Arrow.down => rfl
  Iff.mp (pointwiseEquality (reverse ∘ reverse) id) f

Is there such an axiom in a standard library?

[Kim Morrison]

funext